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

Showing changes from revision #1 to #2: Added | Removed | Changed

(homotopy) category theory(homotopy) type theorycoq
semanticssyntaxidentifier
object classifier Ω\OmegaTypeTypeType
object XXtype x:Xx : X
fibration(display map) A p X\array{A \\ \downarrow^{\mathrlap{p}} \\ X}dependent type x:XA(x):Typex : X \vdash A(x) : Typex : X - P x : Type
section X t A id p X\array{ X &&\stackrel{t}{\to}&& A \\ & {}_{\mathllap{id}}\searrow && \swarrow_{p} \\ && X}term x:Xt(x):A(x)x : X \vdash t(x) : A(x)
pullback f *A A p Y f X\array{ f^* A &\to& A \\ \downarrow && \downarrow^{\mathrlap{p}} \\ Y &\stackrel{f}{\to} & X }substitution y:YA(f(y)):Typey : Y \vdash A(f(y)) : Type
direct image A f *A p f *p X f Y\array{ A && f_* A \\ {}^{\mathllap{p}}\downarrow && \downarrow ^{f_* p}\\ X &\stackrel{f}{\to}& Y}dependent product y:Yx:X(y)A(x):Type y : Y \vdash \underset{x : X(y)}{\prod } A(x) : Type
internal hom in slice X×f *A f *f *A =[X,A] Y X f Y\array{ X \times f^* A && f_* f^* A & = [X,A]_Y \\ {}^{\mathllap{}}\downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}function type y:YX(y)A(y):Type y : Y \vdash X(y) \to A(y) : Type
postcomposition A = f !A X f Y\array{ A &=& f_! A \\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}dependent sum y:Yx:X(y)A(x):Typey : 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
fiberproduct X×f *A = f !f *A =X× YA X f Y\array{ X \times f^* A &=& f_! f^* A & = X \times_Y A\\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}product type y:YX(y)×A(y):Typey : Y \vdash X(y) \times A(y) : Type
Beck-Chevalley condition of codomain fibrationsubstitution commutes with dependent sum
path space object A I (d 1,d 0) A×A\array{A^I \\ \downarrow^{\mathrlap{(d_1,d_0)}} \\ A \times A}identity type a,b:A(a=b)a,b : A \vdash (a = b)
(-2)-truncated morphism/equivalence Y X\array{Y \\ \downarrow^{\mathrlap{\simeq}} \\ X}true/unit type x:X1:Typex : X \vdash 1 : Type
(-1)-truncated morphism/monomorphism ϕ X\array{\phi \\ \downarrow \\ X}proposition x:Xϕ(x):Typex : X \vdash \phi(x) : Type
direct image of (-1)-truncated morphismuniversal quantifier y:YxX(y)ϕ(x):Typey : Y \vdash \underset{x \in X(y)}{\forall} \phi(x) : Typeforall x : X, P x
(-1)-truncation of postcomposition of (-1)-truncated morphismexistential quantifier y:YxX(y)ϕ(x)y : Y \vdash \underset{x \in X(y)}{\exists} \phi(x) exists x : X, P x
texttext

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.