Twan van Laarhoven
Me
Publications
Software
Blog
Posts tagged 'hott'
Date:
2018-01-04
Tags: hott, ttie
0 comments
Type theory with indexed equality - the theory
The theory behind TTIE
Date:
2017-04-06
Tags: hott, ttie
3 comments
A type theory based on indexed equality - Implementation
The TTIE language
Date:
2014-07-01
Tags: hott
0 comments
Dependent equality with the interval
Equating two values with types on two sides of the interval
Date:
2013-07-04
Tags: agda, hott
0 comments
cong from refl in univalent OTT
... and hence subst from refl
Date:
2013-06-22
Tags: agda, hott
1 comment
Substitution from congruence in univalent OTT
It is sufficient to assume `cong` in order to get all properties of identity types