Spahn dictionary Ho CT-Ho TT (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

(homotopy) category theory	(homotopy) type theory	coq
semantics	syntax	identifier
object classifier $\Omega$	Type	~~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)$
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$	`{ 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)$
(-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`


text	text

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