 19 Jul, 2020 1 commit


Raphaël Cauderlier authored

 03 Feb, 2018 1 commit


Raphael Cauderlier authored

 16 Feb, 2017 1 commit


Raphael Cauderlier authored

 28 Jul, 2016 4 commits


Raphaël Cauderlier authored

Raphaël Cauderlier authored

Raphaël Cauderlier authored

Raphaël Cauderlier authored

 22 Feb, 2016 3 commits


Raphaël Cauderlier authored

Raphaël Cauderlier authored
abstractions so we annotate them

Raphaël Cauderlier authored
inductionrecursion which simplifies much the development. Equality, reflexivity and induction principle are mutually defined because of the tricky case of dependent sums (which we need to define equivalence). The computational behaviour of induction principle is given prior to its definition and introduces a lot of critical pairs which should be checked one by one. To simplify this, we treat as much as possible type constructors as derived. The type 2 is not used for the development but it is quite trivial. The main missing feature with respect to usual type theory is the construction of inductive types. Maybe Wtypes could be added without too much pain, this will probably be useful for testing purposes.

 19 Feb, 2016 3 commits


Raphaël Cauderlier authored

Raphaël Cauderlier authored

Raphaël Cauderlier authored
Equality is defined by patternmatching on types and univalence is proved assuming some form of extensionnality
