groupid laws

0Trinitarianism/Quest4Solutions.agda

@@ -1,7 +1,70 @@
 module 0Trinitarianism.Quest4Solutions where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
 
-data _≣_ {A : Type} : (x y : A) → Type where
+data Id {A : Type} : (x y : A) → Type where
 
-  rfl : (x : A) → x ≣ x
+  rfl : {x : A} → Id x x
+
+idSym : (A : Type) (x y : A) → Id x y → Id y x
+idSym A x .x rfl = rfl
+
+Sym : {A : Type} {x y : A} → Id x y → Id y x
+Sym rfl = rfl
+
+_*_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
+rfl * q = q
+
+_*0_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
+p *0 rfl = p
+
+_*1_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
+rfl *1 rfl = rfl
+
+data _×_ (A B : Type) : Type where
+
+  _,_ : A → B → A × B
+
+id× : {A B : Type} (a0 a1 : A) (b0 b1 : B) →
+  (Id a0 a1 × Id b0 b1) ≅ Id {A × B} ( a0 , b0 ) ( a1 , b1 )
+id× {A} {B} a0 a1 b0 b1 = iso fun inv rightInv leftInv where
+
+  fun : Id a0 a1 × Id b0 b1 → Id {A × B} ( a0 , b0 ) ( a1 , b1 )
+  fun (rfl , rfl) = rfl
+
+  inv : Id {A × B} ( a0 , b0 ) ( a1 , b1 ) → Id a0 a1 × Id b0 b1
+  inv rfl = rfl , rfl
+
+  rightInv : section fun inv
+  rightInv rfl = refl
+
+  leftInv : retract fun inv
+  leftInv (rfl , rfl) = refl
+
+------------Cong-------------------------
+
+private
+  variable
+    A B : Type
+
+Cong : {x y : A} (f : A → B) → Id x y → Id (f x) (f y)
+Cong f rfl = rfl
+
+------------Groupoid Laws----------------
+
+rfl* : {x y : A} (p : Id x y) → Id (rfl * p) p
+rfl* p = rfl
+
+*rfl : {x y : A} (p : Id x y) → Id (p * rfl) p
+*rfl rfl = rfl
+
+*Sym : {A : Type} {x y : A} (p : Id x y) → Id (p * Sym p) rfl
+*Sym rfl = rfl
+
+Sym* : {A : Type} {x y : A} (p : Id x y) → Id rfl (p * Sym p)
+Sym* rfl = rfl
+
+Assoc : {A : Type} {w x y z : A} (p : Id w x) (q : Id x y) (r : Id y z)
+        → Id ((p * q) * r) (p * (q * r))
+Assoc rfl q r = rfl