aboutsummaryrefslogtreecommitdiff
path: root/HoTT.thy
diff options
context:
space:
mode:
authorJosh Chen2018-08-06 23:56:10 +0200
committerJosh Chen2018-08-06 23:56:10 +0200
commit4bab3b7f757f7cfbf86ad289b9d92b19a987043a (patch)
treee7af54428ac7a4f7129d3478b96ebf4152c4d201 /HoTT.thy
parentf0234b685d09a801f83a7db91c94380873832bd5 (diff)
Partway through changing function application syntax style.
Diffstat (limited to '')
-rw-r--r--HoTT.thy4
1 files changed, 3 insertions, 1 deletions
diff --git a/HoTT.thy b/HoTT.thy
index fa50f61..ce77ec7 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -12,9 +12,11 @@ HoTT_Base
HoTT_Methods
(* Types *)
-Equal
Prod
Sum
+Equal
+Coprod
+Nat
(* Additional properties *)
EqualProps