Skip to main content
Get your Wikispaces Classroom now:
the easiest way to manage your class.
Pages and Files
Categorical Semantics WG
Coq for UF
Coq Working Group
Formalized Homotopy Theory
Higher Inductive Types
Homotopy Type System
how to add a plugin
IAS program participants
Informal Type Theory
Math in HoTT
Modal type theory
Notation and terminology
Add "All Pages"
Outline of the proof assistant
What I am writing up now looks approximately as follows:
It is a type system or, to be more precise, a family of type systems parametrized by pairs (UC, FV) where UC is a "universe context" and FV a sequence of formal type variables. The type systems of this family corresponding to sensible UC (which is a well defined and decidable property) and empty FV have univalent model.
It has three classes of expressions - u-level expressions (corresponding to universe levels), T-expressions (corresponding to types) and o-expressions (corresponding to objects of types).
It has universes, dependent products, unit type, dependent sums, empty type, pairwise disjoint unions, generalized W-types (corresponding to parametrized containers) and identity types. It has resizing rules.
It has unique typing. More precisely for a given context G and a given o-term o there is an easily computable T-term \tau_G(o) which is the type of o in G.
It is expected to have canonicity for disjoint unions and generalized W-types.
It has stronger definitional equality than most other intensional type systems. In particular, it has eta-rule for all type constructors listed above other than the identity types.
This makes definitional equality to be context dependent and undecidable. Therefore sentences (sequents) can not be internally represented syntactically (i.e. as sequences of terms) because it is impossible to mechanically verify derivability in such presentation.
This is approximately where I am now - thinking about the way to represent sentences (theorems, proofs) in a way which would allow for mechanical verification of derivability. At the moment I am considering the possibility to represent sentences directly by their derivation trees.
Since definitional equality is context dependent and undecidable anyway one can play with many ideas related to making it even stronger e.g. by adding functional extensionality. I think that canonicity can still be preserved, at least for natural numbers, because in the presence of eta-rule for nat propositional equality in nat implies definitional equality.
help on how to format text
Turn off "Getting Started"