aboutsummaryrefslogtreecommitdiff
path: root/ex/HoTT book
diff options
context:
space:
mode:
authorJosh Chen2018-08-16 16:11:42 +0200
committerJosh Chen2018-08-16 16:13:33 +0200
commit8ed9cf8682c07fc47b86c2d0aaeb8b4628aeaa31 (patch)
tree8aad54e91d8174a4fe4d24443d5ad120612ec2e2 /ex/HoTT book
parentca8e7a2681c133abdd082cfa29d6994fa73f2d47 (diff)
Prod.thy now has the correct definitional equality structure rule. Definition of function composition and properties.
Diffstat (limited to 'ex/HoTT book')
0 files changed, 0 insertions, 0 deletions