projects / cubicaltt.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5538154) | patch
define equivalence using Id and prove univalence with Id everywhere
authorAnders Mörtberg <andersmortberg@gmail.com>
Fri, 29 Jul 2016 12:12:07 +0000 (14:12 +0200)
committerAnders Mörtberg <andersmortberg@gmail.com>
Fri, 29 Jul 2016 12:12:07 +0000 (14:12 +0200)
commit53541cdc8e06d291dfbf614a3b00f15935f81d4f
treeb1d4770e136e059552a7cf0e8b23c46b1a679a4ctree | snapshot
parent553815428a8d07a6510bc4623a331313ce5ecb78commit | diff
define equivalence using Id and prove univalence with Id everywhere
examples/idtypes.ctt diff | blob | blame | history
examples/prelude.ctt diff | blob | blame | history
My fork of cubicaltt with web interface using Reflex.