aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy
diff options
context:
space:
mode:
authorJosh Chen2018-06-18 17:16:30 +0200
committerJosh Chen2018-06-18 17:16:30 +0200
commit21077433667f6c2281aa522f170b93bb0c8c23ea (patch)
tree75160b85debd56aa2151f2a0787e9973c31228a6 /HoTT.thy
parent912a4a4b909041cb280ae5cecd40867ce34b58de (diff)
Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Added type formation rules expressing necessity of the conditions.
Diffstat (limited to 'HoTT.thy')
0 files changed, 0 insertions, 0 deletions