Showing changes from revision #1 to #2:
Added | Removed | Changed
This entry is about
Bart Jacobs, categorical logic and type theory
11.5 Full higher order dependent type theory (Fho DTT)
(p.684)
Definition (dependency): (…) reads “ depends on ”.
In Fho DTT we have: , , , and . It is a main difference to polymorphic dependent type theory (PDTT) that there we do not have .
For sorts such that the -product resp. -sum resp. equality rules are defined by
The weak elimination rule for -sums is
(…)
11.6 Fho DTT categorically
(p.692)
First we import a definition from §9:
Definition (p.539): Let be a fibration. A functor is called a comprehension category on if we have:
(1) . (2) For each cartesian map in, the induced square in is a pullback.
Definition (p.694): A weak Fho DTT-structure is defined to be a diagram
where
is a closed comprehension category of kinds.
is a fibration (of types), and is a fibered reflection.
There is an object over .
In this case the composite is a comprehension category which has a unit where is the unit of .
The following example of an is a degenerate one since the subobject fibration for types is a poset.
Example (p.695): Let be a topos. Then is a regular category, such that there is a fibered reflection as in Theorem 4.4.4. where the reflector sends a morphism to its monic part (using the epi-mono factorization in a topos). Since monos are closed under composition, is a closed comprehension category. So we obtain a Fho DTT-structure
Last revised on February 19, 2013 at 03:25:07.
See the history of this page for a list of all contributions to it.