natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
In dependent type theory, the binary pullback type of functions $f:A \to C$ and $g:B \to C$ is given by the type
However, by using large elimination of the boolean domain $\mathrm{bool}$ on the codomain of the functions and by using the induction principle for the boolean domain on the functions themselves, one has a family of functions
and the resulting binary pullback is the type
Thus, it suffices to define the binary pushout of a boolean-indexed family of functions $f:\prod_{x:\mathrm{bool}} A(x) \to C$, which is the type
For any elements $x:A$ and $y:A$, the identity type $x = y$ is equivalent to the dependent sum type $\sum_{z:A} (x = z) \times (y = z)$, and so the pullback is equivalently the type
and since dependent sum types and product types commute, this is equivalently the type
By induction on the booleans, this is equivalently
By generalizing this definition of binary pullbacks from the boolean domain to any arbitrary type, one gets general dependent pullbacks of an arbitrary family of functions with codomain $C$, which are also known as wide pullbacks in category theory.
Given a type $C$, an index type $I$, a family of domains $A(i)$ indexed by $i:I$, and a family of functions $f:\prod_{i:I} A(i) \to C$, the dependent pullback type or wide pullback type of $(C, I, A, f)$ is the dependent sum type
The type $\sum_{x:A(i)} f(i, x) =_C y$ is the fiber type of the function $f(i):A(i) \to C$ at the element $y:C$, so this type is also the dependent product of fiber types, or the dependent fiber product type or dependent fibre product type.
In addition, there is a dependent function
which shows that the dependent pullback type is a wide span.
The dependent product type of a family of types $B(x)$ indexed by $x:A$ is the dependent pullback of the family of unique functions from each $B(x)$ to the unit type.
The intersection of a family of subtypes of a type $A$ is given by the dependent pullback of the embeddings into $A$.
Binary pullback types? are boolean-indexed dependent pullbacks types.
When the family of domains $A(x)$ indexed by $x:I$ is a constant family of types, then the dependent pullback type are called dependent equalizer types or wide equalizer types.
Last revised on February 11, 2024 at 18:03:08. See the history of this page for a list of all contributions to it.