# Spahn dictionary Ho CT-Ho TT (Rev #1)

(homotopy) category theory(homotopy) type theorycoq
semanticssyntaxidentifier
object classifier $\Omega$TypeType
object $X$type $x : X$
fibration(display map) $\array{A \\ \downarrow^{\mathrlap{p}} \\ X}$dependent type $x : X \vdash A(x) : Type$
section $\array{ X &&\stackrel{t}{\to}&& A \\ & {}_{\mathllap{id}}\searrow && \swarrow_{p} \\ && X}$term $x : X \vdash t(x) : A(x)$
pullback $\array{ f^* A &\to& A \\ \downarrow && \downarrow^{\mathrlap{p}} \\ Y &\stackrel{f}{\to} & X }$substitution $y : Y \vdash A(f(y)) : Type$
direct image $\array{ A && f_* A \\ {}^{\mathllap{p}}\downarrow && \downarrow ^{f_* p}\\ X &\stackrel{f}{\to}& Y}$dependent product $y : Y \vdash \underset{x : X(y)}{\prod } A(x) : Type$
internal hom in slice $\array{ X \times f^* A && f_* f^* A & = [X,A]_Y \\ {}^{\mathllap{}}\downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}$function type $y : Y \vdash X(y) \to A(y) : Type$
postcomposition $\array{ A &=& f_! A \\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}$dependent sum $y : Y \vdash \underset{x : X(y)}{\sum} A(x) : Type$
fiberproduct $\array{ X \times f^* A &=& f_! f^* A & = X \times_Y A\\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}$product type $y : Y \vdash X(y) \times A(y) : Type$
Beck-Chevalley condition of codomain fibrationsubstitution commutes with dependent sum
path space object $\array{A^I \\ \downarrow^{\mathrlap{(d_1,d_0)}} \\ A \times A}$identity type $a,b : A \vdash (a = b)$
(-2)-truncated morphism/equivalence $\array{Y \\ \downarrow^{\mathrlap{\simeq}} \\ X}$true/unit type $x : X \vdash 1 : Type$
(-1)-truncated morphism/monomorphism $\array{\phi \\ \downarrow \\ X}$proposition $x : X \vdash \phi(x) : Type$
direct image of (-1)-truncated morphismuniversal quantifier $y : Y \vdash \underset{x \in X(y)}{\forall} \phi(x) : Type$
(-1)-truncation of postcomposition of (-1)-truncated morphismexistential quantifier $y : Y \vdash \underset{x \in X(y)}{\exists} \phi(x)$

Revision on November 15, 2012 at 15:06:28 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.