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

(homotopy) category theory	(homotopy) type theory	coq
semantics	syntax	identifier
object classifier $\Omega$	Type	Type
object $X$	type $x : X$
fibration(display map) $\array{A \\ \downarrow^{\mathrlap{p}} \\ X}$	dependent type $x : X \vdash A(x) : Type$	x : X \| - P x : Type
section $\array{ X &&\stackrel{t}{\to}&& A \\ & {}_{\mathllap{id}}\searrow && \swarrow_{p} \\ && X}$	term $x : X \vdash t(x) : A(x)$	X : Type
pullback $\array{ f^* A &\to& A \\ \downarrow && \downarrow^{\mathrlap{p}} \\ Y &\stackrel{f}{\to} & X }$	substitution $y : Y \vdash A(f(y)) : Type$	{y : Y & {a : A & f y ~~> p a}}
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$	{ x : X & P x } : Type $or$ sig T (fun (x : X) => P x) : Type. $or$ sig T P : Type
fiber product $\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 fibration	substitution 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)$	paths X : X -> X -> Type Id X : X -> X -> Type
(-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 morphism	universal quantifier $y : Y \vdash \underset{x \in X(y)}{\forall} \phi(x) : Type$	forall x : X, P x
(-1)-truncation of postcomposition of (-1)-truncated morphism	existential quantifier $y : Y \vdash \underset{x \in X(y)}{\exists} \phi(x)$	exists x : X, P x

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