hlevel additions (RedPRL#167)

test/hlevel.cooltt

@@ -20,6 +20,9 @@ def has-hlevel : nat → type → type =
   | suc l => aux l
   ]
 
+def is-set : type → type = has-hlevel 2
+def is-groupoid : type → type = has-hlevel 3
+
 def hLevel (n : nat) : type =
   (A : type) × has-hlevel n A
 
@@ -29,3 +32,26 @@ def hGroupoid : type = hLevel 3
 
 print hProp
 normalize hProp
+
+def symm/filler (A : type) (p : 𝕀 → A) (i : 𝕀) : 𝕀 → A =
+  hfill A 0 {∂ i} {j _ =>
+    [ j=0 ∨ i=1 => p 0
+    | i=0 => p j
+    ]
+  }
+
+def symm (A : type) (p : 𝕀 → A) : path A {p 1} {p 0} =
+  i => symm/filler A p i 1
+
+def trans/filler (A : type) (p : 𝕀 → A) (q : (i : 𝕀) → sub A {i=0} {p 1}) (j : 𝕀) (i : 𝕀) : A =
+  hcom A 0 j {∂ i} {j _ =>
+    [ j=0 ∨ i=0 => p i
+    | i=1 => q j
+    ]
+  }
+
+def trans (A : type) (p : 𝕀 → A) (q : (i : 𝕀) → sub A {i=0} {p 1}) : path A {p 0} {q 1} =
+  trans/filler A p q 1
+
+def contr-prop (A : type) (A/contr : is-contr A) : is-prop A =
+  a a' => trans A {symm A {{snd A/contr} a}} {{snd A/contr} a'}