cubical type theory in nLab

ncatlab.org · 2,370 words · saved by 1 readers

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory homotopy levels type theory 2-type theory, 2-categorical logic homotopy type theory, homotopy type theory - contents homotopy type univalence, function extensionality, internal logic of an (∞,1)-topos cohesive homotopy type theory directed homotopy type theory HoTT methods for homotopy theorists semantics internal logic, categorical semantics internal logic of a topos Mitchell-Benabou language Kripke-Joyal semantics internal logic of an (∞,1)-topos Edit this sidebar Cubical type theory is a flavor of dependent type theory in which maps out of an interval primitive is used to define cubical path types, rather than the inductive family of Martin-Löf identity types as in Martin-Löf type theory. Cubical type theory additionally differs from Martin-Löf type theory in that function extensionality is a theorem in cubical type theory, rather than an axiom as is the case in Martin-

cubical type theory in nLab nLab cubical type theory Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Discuss this page | Context Type theory natural deduction metalanguage , practical foundations judgement hypothetical judgement , sequent antecedents ⊢ \vdash consequent , succedents type formation rule term introduction rule term elimination rule computation rule type theory ( dependent , intensional , observational type theory , homotopy type theory ) calculus of constructions syntax object language theory , axiom proposition / type ( propositions as types ) definition

cubical type theory in nLab

related reading