Twan van Laarhoven
Me
Publications
Software
Blog
Posts tagged 'agda'
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
Date:
2013-05-23
Tags: agda
9 comments
The complete correctness of sorting
Merge sort returns an ordered permutation of the input, in O(n * log n).