From ca1a85edf21e0b4fb62d1af716e7a9114a5e64fe Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <amarasep@mcmaster.ca>
Date: Wed, 7 Jan 2026 18:53:52 -0500
Subject: [PATCH 01/18] Compiled Magma Type Definition

---
 test/hott0.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/hott0.lean b/test/hott0.lean
index cb0fd93b..cc560d49 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -60,3 +60,6 @@ hott0
   /-- The univalence axiom for sets. See HoTT book, Axiom 2.10.3. -/
   axiom setUv₀₀ {A B : Type} (A_set : isSet₀ A) (B_set : isSet₀ B) :
     isEquiv₁₀ (@Identity.toEquiv₀₀ A B)
+
+-- Beginning Magma Definition
+hott0 def magma (A : Type) : Type :=  A → A → A

From abbbaf75411f49c7b4176377d232ef266557c6c8 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <amarasep@mcmaster.ca>
Date: Wed, 14 Jan 2026 20:22:49 -0500
Subject: [PATCH 02/18] Modified Magma Def:

---
 test/hott0.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index cc560d49..d6dcdc22 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -62,4 +62,4 @@ hott0
     isEquiv₁₀ (@Identity.toEquiv₀₀ A B)
 
 -- Beginning Magma Definition
-hott0 def magma (A : Type) : Type :=  A → A → A
+hott0 def magma :=  Σ (A : Type), A → A → A

From ec9c259a4c5b0b2fc0ccc10aa682210be26770b4 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Mon, 19 Jan 2026 22:57:56 -0500
Subject: [PATCH 03/18] Adding Some new Targets to prove, in sequence

---
 test/hott0.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index d6dcdc22..27412e7d 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -62,4 +62,14 @@ hott0
     isEquiv₁₀ (@Identity.toEquiv₀₀ A B)
 
 -- Beginning Magma Definition
-hott0 def magma :=  Σ (A : Type), A → A → A
+hott0 def magma :=  Σ (A : Type), A → (A → A)
+
+-- Recall Currying
+-- Prove by Hand
+
+
+-- Hedberg's Rijke 12.3.5
+-- hott0 theorem hedberg₀ {A : Type} (Π x, y : A) (x =y) + (x ≠ y)
+-- that A has decidable equality. Furthermore, let U be a universe containing
+-- the type A. We will prove that A is a set by Applying Theorem 12.3.4
+

From 1fa5a812ac871ec467a52eb1b8ac8434df889e58 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <pesaraamarasekera@Pesaras-MacBook-Air.local>
Date: Tue, 20 Jan 2026 11:17:22 -0500
Subject: [PATCH 04/18] Merging

---
 test/hott0.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/test/hott0.lean b/test/hott0.lean
index d6dcdc22..be1b7414 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -63,3 +63,7 @@ hott0
 
 -- Beginning Magma Definition
 hott0 def magma :=  Σ (A : Type), A → A → A
+
+-- Retrying how to solve the pull request for issue
+-- Prove that equivalent magmas consisting of set-data (meaning magmas
+-- (A,A×A→A) s.t. the underlying type A is a set) are equal using set-univalence in test/hott0.lean.

From 24e3d8282ce404a23de98e9440e50352f5c9975c Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Wed, 21 Jan 2026 18:03:12 -0500
Subject: [PATCH 05/18] Sepearated work in Hedberg

---
 test/hott0.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index fdc55425..b75e77ea 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -67,12 +67,3 @@ hott0 def magma :=  Σ (A : Type), A → (A → A)
 -- Retrying how to solve the pull request for issue
 -- Prove that equivalent magmas consisting of set-data (meaning magmas
 -- (A,A×A→A) s.t. the underlying type A is a set) are equal using set-univalence in test/hott0.lean.
-
--- Recall Currying
--- Prove by Hand
-
-
--- Hedberg's Rijke 12.3.5
--- hott0 theorem hedberg₀ {A : Type} (Π x, y : A) (x =y) + (x ≠ y)
--- that A has decidable equality. Furthermore, let U be a universe containing
--- the type A. We will prove that A is a set by Applying Theorem 12.3.4

From 7976197299850422064d8cd6fa3c040173953463 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Wed, 21 Jan 2026 18:19:08 -0500
Subject: [PATCH 06/18] Adding Projection operators

---
 test/hott0.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/test/hott0.lean b/test/hott0.lean
index b75e77ea..fb643f60 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -64,6 +64,27 @@ hott0
 -- Beginning Magma Definition
 hott0 def magma :=  Σ (A : Type), A → (A → A)
 
+-- Projection helpers
+hott0 def magma.carrier (M : magma) : Type := M.1
+hott0 def magma.op (M : magma) : M.carrier → M.carrier → M.carrier := M.2
+
+
+
 -- Retrying how to solve the pull request for issue
 -- Prove that equivalent magmas consisting of set-data (meaning magmas
 -- (A,A×A→A) s.t. the underlying type A is a set) are equal using set-univalence in test/hott0.lean.
+-- A magma homomorphism preserves the operation
+hott0 def magma_hom (M N : magma) : Type :=
+  Σ (f : M.carrier → N.carrier),
+    ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
+
+-- A magma equivalence is an equivalence that preserves structure
+hott0 def magma_equiv (M N : magma) : Type :=
+  Σ (f : M.carrier → N.carrier),
+    Σ (e : isEquiv₀₀ f),
+      ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
+
+-- Or the uncurried version
+hott0 def Sigma.eta {A : Type} {B : A → Type} (w : Σ (a : A), B a) :
+    Identity w ⟨w.1, w.2⟩ :=
+  .rfl₀

From 515faeee633b99adce277586e7062026e644fcb2 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Wed, 21 Jan 2026 18:22:08 -0500
Subject: [PATCH 07/18] Removed uncurried comment

---
 test/hott0.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index fb643f60..d193e75a 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -84,7 +84,6 @@ hott0 def magma_equiv (M N : magma) : Type :=
     Σ (e : isEquiv₀₀ f),
       ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
 
--- Or the uncurried version
 hott0 def Sigma.eta {A : Type} {B : A → Type} (w : Σ (a : A), B a) :
     Identity w ⟨w.1, w.2⟩ :=
   .rfl₀

From a74c705a536be620404dc59dcc1bee934e7d20b5 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Thu, 22 Jan 2026 13:49:32 -0500
Subject: [PATCH 08/18] Added Carriers, Eta for Sigma, Postulated proof

---
 test/hott0.lean | 49 +++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 45 insertions(+), 4 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index d193e75a..9305abd5 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -50,6 +50,9 @@ hott0 def isEquiv₀₀_transport₀ {A B : Type} (h : Identity A B) : isEquiv
 hott0 def Identity.toEquiv₀₀ {A B : Type} : Identity A B → Σ (f : A → B), isEquiv₀₀ f :=
   fun h => ⟨transport₀ h, isEquiv₀₀_transport₀ h⟩
 
+--Adding Is Contractible over here
+hott0 def isContr₀ (A : Type) : Type := sorry
+
 hott0 def isProp₀ (A : Type) : Type :=
   ∀ (a a' : A) (h h' : Identity a a'), Identity h h'
 
@@ -65,11 +68,11 @@ hott0
 hott0 def magma :=  Σ (A : Type), A → (A → A)
 
 -- Projection helpers
+-- The set
 hott0 def magma.carrier (M : magma) : Type := M.1
+ -- The Operation
 hott0 def magma.op (M : magma) : M.carrier → M.carrier → M.carrier := M.2
 
-
-
 -- Retrying how to solve the pull request for issue
 -- Prove that equivalent magmas consisting of set-data (meaning magmas
 -- (A,A×A→A) s.t. the underlying type A is a set) are equal using set-univalence in test/hott0.lean.
@@ -84,6 +87,44 @@ hott0 def magma_equiv (M N : magma) : Type :=
     Σ (e : isEquiv₀₀ f),
       ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
 
+
+-- Equality of Sigma types
 hott0 def Sigma.eta {A : Type} {B : A → Type} (w : Σ (a : A), B a) :
-    Identity w ⟨w.1, w.2⟩ :=
-  .rfl₀
+    Identity w ⟨w.1, w.2⟩ := Identity.rfl₀
+
+-- hott0 def Sigma.eq {A : Type} {B : A → Type} {w w' : Σ (a : A), B a}
+--     (p : Identity w.1 w'.1)
+--     (q : Identity (transport₀ (p.map B) w.2) w'.2)
+--     : Identity w w' := sorry
+
+-- DepTypes are Problems
+-- theorem statement I think I have to use def instead of theorem
+
+-- Consider Defining a Theorem
+
+-- Consider SIP
+-- Need to ask how they define theorems
+hott0 def magma_eq_of_equiv
+    (M N : magma)
+    (M_set : isSet₀ M.carrier)
+    (N_set : isSet₀ N.carrier)
+    (e : magma_equiv M N)
+    : Identity M N :=
+  -- Steps
+  -- Extract carrier equivalence (both types and operations are equiv/iso)
+  let  ⟨f, f_equiv, f_hom⟩ := e
+  -- Use set uni to get M.carrier = N.carrier
+  have carrier_eq : Identity M.carrier N.carrier := by
+    let ⟨g_inv, _, _, _⟩ := setUv₀₀ M_set N_set
+    exact g_inv ⟨f, f_equiv⟩
+  -- Use Sigma.eta (Dep Pair Type equality) to construct M = N
+  have op_eq : Identity (transport₀ (sorry : Identity _ _) M.op) N.op := by
+    --apply funext₀₀; intro ⟨x, y⟩
+    sorry
+  -- Show operations are equal
+  sorry
+  --exact
+  -- exact Sigma.eta carrier_eq op_eq
+
+-- What makes something exactly a def
+-- Why should we use def vs theorem??

From e2b0baca356add9facb7530dba7caa6722f450e8 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Thu, 22 Jan 2026 13:51:18 -0500
Subject: [PATCH 09/18] Forgot to add this in the last one commit

---
 test/hott0.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index 9305abd5..16f6438c 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -88,10 +88,11 @@ hott0 def magma_equiv (M N : magma) : Type :=
       ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
 
 
--- Equality of Sigma types
+-- Equality of Sigma types, using currying
 hott0 def Sigma.eta {A : Type} {B : A → Type} (w : Σ (a : A), B a) :
     Identity w ⟨w.1, w.2⟩ := Identity.rfl₀
 
+
 -- hott0 def Sigma.eq {A : Type} {B : A → Type} {w w' : Σ (a : A), B a}
 --     (p : Identity w.1 w'.1)
 --     (q : Identity (transport₀ (p.map B) w.2) w'.2)
@@ -122,9 +123,9 @@ hott0 def magma_eq_of_equiv
     --apply funext₀₀; intro ⟨x, y⟩
     sorry
   -- Show operations are equal
-  sorry
+  --sorry
   --exact
-  -- exact Sigma.eta carrier_eq op_eq
+  exact Σ.eq carrier_eq op_eq
 
 -- What makes something exactly a def
 -- Why should we use def vs theorem??

From 116bcfa664135ccaa1f48f60fd2968f003c48336 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Fri, 23 Jan 2026 14:13:27 -0500
Subject: [PATCH 10/18] Committing rough work before cleanup

---
 test/hott0.lean | 246 +++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 214 insertions(+), 32 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index 16f6438c..ca04b93d 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -50,8 +50,10 @@ hott0 def isEquiv₀₀_transport₀ {A B : Type} (h : Identity A B) : isEquiv
 hott0 def Identity.toEquiv₀₀ {A B : Type} : Identity A B → Σ (f : A → B), isEquiv₀₀ f :=
   fun h => ⟨transport₀ h, isEquiv₀₀_transport₀ h⟩
 
+--- Another addition of mine TODO
 --Adding Is Contractible over here
 hott0 def isContr₀ (A : Type) : Type := sorry
+------
 
 hott0 def isProp₀ (A : Type) : Type :=
   ∀ (a a' : A) (h h' : Identity a a'), Identity h h'
@@ -64,6 +66,118 @@ hott0
   axiom setUv₀₀ {A B : Type} (A_set : isSet₀ A) (B_set : isSet₀ B) :
     isEquiv₁₀ (@Identity.toEquiv₀₀ A B)
 
+
+-- My stuff starts here
+--====================================
+-- Path Algebra stuff
+
+-- ap on one type
+hott0 def ap {A B : Type} (f : A → B) {a a' : A} (p : Identity a a') : Identity (f a) (f a') :=
+  p.rec (Identity.rfl₀)
+
+-- ap on two types
+hott0 def ap₂ {A B C : Type} (f : A → B → C) {a a' : A} {b b' : B}
+    (p : Identity a a') (q : Identity b b') : Identity (f a b) (f a' b') :=
+  p.rec (ap (f a) q)
+
+--=======================================
+--Sigma Type Stuff
+
+-- hott0 def transportPath {A : Type} {B : A → Type} {a a' : A}
+--     (p : Identity a a') (b : B a) : B a' :=
+--   p.rec b
+
+-- Sigma type Eta expansion
+hott0 def Sigma.eta {A : Type} {B : A → Type} (w : Σ (a : A), B a) :
+    Identity w ⟨w.1, w.2⟩ := Identity.rfl₀
+
+
+-- Well this was a bloody nightmare to figure out
+hott0 def Sigma.eq {A : Type} {B : A → Type} {w w' : Σ (a : A), B a}
+    (p : Identity w.1 w'.1)
+    (q : Identity (p.rec w.2) w'.2)
+    : Identity w w' :=
+  @Identity.rec
+    A
+    w.1
+    (fun x p' => ∀ (b' : B x), Identity (p'.rec w.2) b' → Identity w ⟨x, b'⟩)
+    (fun b' q' =>
+      @Identity.rec
+        (B w.1)
+        w.2
+        (fun b'' q'' => Identity w ⟨w.1, b''⟩)
+        Identity.rfl₀
+        b'
+        q')
+    w'.1
+    p
+    w'.2
+    q
+
+-- Sigma eq for Type 1
+hott0 def Sigma.eq₁ {A : Type 1} {B : A → Type} {w w' : Σ (a : A), B a}
+    (p : Identity w.1 w'.1)
+    (q : Identity (p.rec w.2) w'.2)
+    : Identity w w' :=
+  @Identity.rec
+    A
+    w.1
+    (fun x p' => ∀ (b' : B x), Identity (p'.rec w.2) b' → Identity w ⟨x, b'⟩)
+    (fun b' q' =>
+      @Identity.rec
+        (B w.1)
+        w.2
+        (fun b'' q'' => Identity w ⟨w.1, b''⟩)
+        Identity.rfl₁
+        b'
+        q')
+    w'.1
+    p
+    w'.2
+    q
+
+-- hott0 is a custom elaborator that enforces single-definitions
+hott0 def funext₀ {A : Type} {B : A → Type} {f g : (a : A) → B a}
+    (h : ∀ (a : A), Identity (f a) (g a)) : Identity f g :=
+  (funext₀₀ f g).1 h
+
+---================================
+-- Univalence computation rule
+
+hott0
+  /-- Univalence Computation Rule.
+      See HoTT book (Univalent Foundations), Axiom 2.10.3, Remark 2.10.4.
+  -/
+  axiom ua_comp₀₀ {A B : Type}
+    (A_set : isSet₀ A) (B_set : isSet₀ B) (f : A → B) (e : isEquiv₀₀ f) (a : A):
+    --let ⟨ua_inv, _, _, _⟩ := (setUv₀₀ A_set B_set).1
+    Identity (transport₀ ((setUv₀₀ A_set B_set).1 ⟨f, e⟩) a) (f a)
+
+
+--=====================================
+-- Transport on Π-Types
+
+hott0
+  /-- Transport on binary operations -/
+  axiom transport_op {A B : Type}
+      (A_set : isSet₀ A) (B_set : isSet₀ B)
+      (f : A → B) (e : isEquiv₀₀ f)
+      (op : A → A → A) (b₁ b₂ : B) :
+    Identity
+      (@Identity.rec Type A (fun X _ => X → X → X) op B ((setUv₀₀ A_set B_set).1 ⟨f, e⟩) b₁ b₂)
+      (f (op (e.1 b₁) (e.1 b₂)))
+
+
+--For functions with two arguments, we need to apply this twice:
+hott0
+  /-- Retraction: f(g(b)) = b. -/
+  axiom retraction {A B : Type}
+      (A_set : isSet₀ A) (B_set : isSet₀ B)
+      (f : A → B) (e : isEquiv₀₀ f) (b : B) :
+    Identity (f (e.1 b)) b
+
+
+---============================================
 -- Beginning Magma Definition
 hott0 def magma :=  Σ (A : Type), A → (A → A)
 
@@ -77,9 +191,9 @@ hott0 def magma.op (M : magma) : M.carrier → M.carrier → M.carrier := M.2
 -- Prove that equivalent magmas consisting of set-data (meaning magmas
 -- (A,A×A→A) s.t. the underlying type A is a set) are equal using set-univalence in test/hott0.lean.
 -- A magma homomorphism preserves the operation
-hott0 def magma_hom (M N : magma) : Type :=
-  Σ (f : M.carrier → N.carrier),
-    ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
+-- hott0 def magma_hom (M N : magma) : Type :=
+--   Σ (f : M.carrier → N.carrier),
+--     ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
 
 -- A magma equivalence is an equivalence that preserves structure
 hott0 def magma_equiv (M N : magma) : Type :=
@@ -88,16 +202,8 @@ hott0 def magma_equiv (M N : magma) : Type :=
       ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
 
 
--- Equality of Sigma types, using currying
-hott0 def Sigma.eta {A : Type} {B : A → Type} (w : Σ (a : A), B a) :
-    Identity w ⟨w.1, w.2⟩ := Identity.rfl₀
-
-
--- hott0 def Sigma.eq {A : Type} {B : A → Type} {w w' : Σ (a : A), B a}
---     (p : Identity w.1 w'.1)
---     (q : Identity (transport₀ (p.map B) w.2) w'.2)
---     : Identity w w' := sorry
-
+--===========================================
+-- The actual proof
 -- DepTypes are Problems
 -- theorem statement I think I have to use def instead of theorem
 
@@ -105,27 +211,103 @@ hott0 def Sigma.eta {A : Type} {B : A → Type} (w : Σ (a : A), B a) :
 
 -- Consider SIP
 -- Need to ask how they define theorems
-hott0 def magma_eq_of_equiv
+
+-- Maybe use this?
+-- hott0 def isEquiv₀₀_v2 {A B : Type} (f : A → B) : Type :=
+--   Σ (g : B → A),
+--     Σ (_ : ∀ (a : A), Identity (g (f a)) a),  -- section
+--       ∀ (b : B), Identity (f (g b)) b         -- retraction (for same g!)
+
+hott0
+  axiom equiv_retraction {A B : Type}
+      (A_set : isSet₀ A) (B_set : isSet₀ B)
+      (f : A → B) (e : isEquiv₀₀ f) (b : B) :
+    Identity (f (e.1 b)) b
+
+-- Has let's but cleaner
+-- hott0 def magma_eq_of_equiv
+--     (M N : magma)
+--     (M_set : isSet₀ M.carrier)
+--     (N_set : isSet₀ N.carrier)
+--     (e : magma_equiv M N)
+--     : Identity M N :=
+--   -- Steps
+--   -- Extract carrier equivalence (both types and operations are equiv/iso)
+--   let f := e.1
+--   let f_equiv := e.2.1
+--   let f_hom := e.2.2
+--   let g := f_equiv.1
+--   let h := f_equiv.2.1
+--   let α := f_equiv.2.2.1
+--   let β := f_equiv.2.2.2
+
+--   let carrier_eq := (setUv₀₀ M_set N_set).1 ⟨f, f_equiv⟩
+
+--   let op_eq : Identity (@Identity.rec Type M.carrier (fun X _ => X → X → X)
+--   M.op N.carrier carrier_eq) N.op :=
+--       funext₀ (fun x => funext₀ (fun y =>
+--         -- Proof chain:
+--         -- 1. tranported_op x y = f(M.op(g x, g y)) [by transport_op]
+--         -- 2. f(M.op(g x, g y)) = N.op(f(g x), f(g y)) [by f_hom]
+--         -- 3. N.op(f(g x), f(g y)) = N.op(x,y) [by β (retraction)]
+--     let step1 : Identity
+--         (@Identity.rec Type M.carrier (fun X _ => X → X → X)
+--           M.op N.carrier carrier_eq x y)
+--         (f (M.op (g x) (g y))) :=
+--       transport_op M_set N_set f f_equiv M.op x y
+
+--     let step2 : Identity
+--         (f (M.op (g x) (g y)))
+--         (N.op (f (g x)) (f (g y))) :=
+--       f_hom (g x) (g y)
+
+--     let step3 : Identity
+--         (N.op (f (g x)) (f (g y)))
+--         (N.op x y) :=
+--       ap₂ N.op
+--         (equiv_retraction M_set N_set f f_equiv x)
+--         (equiv_retraction M_set N_set f f_equiv y)
+--     -- Finally, combine to get full equality of magmas
+--     step1.trans₀ (step2.trans₀ step3)
+--     ))
+--   -- Simply combine the two equalities into a Sigma equality to finish
+--   Sigma.eq₁ carrier_eq op_eq
+
+-- What makes something exactly a def
+-- Why should we use def vs theorem??
+
+-- Without let's but not as clean
+-- Helper definitions to break up the complexity
+set_option maxHeartbeats 5000000
+
+hott0 def magma_carrier_eq
     (M N : magma)
     (M_set : isSet₀ M.carrier)
     (N_set : isSet₀ N.carrier)
     (e : magma_equiv M N)
-    : Identity M N :=
-  -- Steps
-  -- Extract carrier equivalence (both types and operations are equiv/iso)
-  let  ⟨f, f_equiv, f_hom⟩ := e
-  -- Use set uni to get M.carrier = N.carrier
-  have carrier_eq : Identity M.carrier N.carrier := by
-    let ⟨g_inv, _, _, _⟩ := setUv₀₀ M_set N_set
-    exact g_inv ⟨f, f_equiv⟩
-  -- Use Sigma.eta (Dep Pair Type equality) to construct M = N
-  have op_eq : Identity (transport₀ (sorry : Identity _ _) M.op) N.op := by
-    --apply funext₀₀; intro ⟨x, y⟩
-    sorry
-  -- Show operations are equal
-  --sorry
-  --exact
-  exact Σ.eq carrier_eq op_eq
+    : Identity M.carrier N.carrier :=
+  (setUv₀₀ M_set N_set).1 ⟨e.1, e.2.1⟩
 
--- What makes something exactly a def
--- Why should we use def vs theorem??
+-- Try a simpler intermediate definition
+hott0 def transported_op
+    (M N : magma)
+    (M_set : isSet₀ M.carrier)
+    (N_set : isSet₀ N.carrier)
+    (e : magma_equiv M N)
+    : N.carrier → N.carrier → N.carrier :=
+  @Identity.rec Type M.carrier (fun X _ => X → X → X)
+    M.op N.carrier (magma_carrier_eq M N M_set N_set e)
+
+hott0 def magma_op_eq_pointwise
+    (M N : magma)
+    (M_set : isSet₀ M.carrier)
+    (N_set : isSet₀ N.carrier)
+    (e : magma_equiv M N)
+    (x y : N.carrier)
+    : Identity (transported_op M N M_set N_set e x y) (N.op x y) :=
+    -- sorry -- this keeps timing out
+  (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
+    ((e.2.2 (e.2.1.1 x) (e.2.1.1 y)).trans₀
+      (ap₂ N.op
+        (equiv_retraction M_set N_set e.1 e.2.1 x)
+        (equiv_retraction M_set N_set e.1 e.2.1 y)))

From 7e99255b0ebf17b4fa07937004f6c864c4412e09 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Fri, 23 Jan 2026 14:39:10 -0500
Subject: [PATCH 11/18] Added proof walkthrough for magma equality

---
 test/hott0.lean | 138 +++++++++++++++++-------------------------------
 1 file changed, 49 insertions(+), 89 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index ca04b93d..ef59e229 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -83,10 +83,6 @@ hott0 def ap₂ {A B C : Type} (f : A → B → C) {a a' : A} {b b' : B}
 --=======================================
 --Sigma Type Stuff
 
--- hott0 def transportPath {A : Type} {B : A → Type} {a a' : A}
---     (p : Identity a a') (b : B a) : B a' :=
---   p.rec b
-
 -- Sigma type Eta expansion
 hott0 def Sigma.eta {A : Type} {B : A → Type} (w : Σ (a : A), B a) :
     Identity w ⟨w.1, w.2⟩ := Identity.rfl₀
@@ -168,15 +164,6 @@ hott0
       (f (op (e.1 b₁) (e.1 b₂)))
 
 
---For functions with two arguments, we need to apply this twice:
-hott0
-  /-- Retraction: f(g(b)) = b. -/
-  axiom retraction {A B : Type}
-      (A_set : isSet₀ A) (B_set : isSet₀ B)
-      (f : A → B) (e : isEquiv₀₀ f) (b : B) :
-    Identity (f (e.1 b)) b
-
-
 ---============================================
 -- Beginning Magma Definition
 hott0 def magma :=  Σ (A : Type), A → (A → A)
@@ -196,27 +183,54 @@ hott0 def magma.op (M : magma) : M.carrier → M.carrier → M.carrier := M.2
 --     ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
 
 -- A magma equivalence is an equivalence that preserves structure
-hott0 def magma_equiv (M N : magma) : Type :=
-  Σ (f : M.carrier → N.carrier),
-    Σ (e : isEquiv₀₀ f),
-      ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
 
+/-
+
+Proof Idea
+------------
+Two magmas are given thus
+M = (A, m) where A is a set and m : A → A → A
+N = (B, n) where B is a set and n : B → B → B
 
---===========================================
--- The actual proof
--- DepTypes are Problems
--- theorem statement I think I have to use def instead of theorem
+We have an equivalence of types e : A ≃ B
+with forward map f : A → B and inverse map g : B → A
 
--- Consider Defining a Theorem
+We have e : isEquiv₀₀ f which gives us:
+1. g : B → A (inverse)
+2. h : B → A (another inver)
+3. α : isSection₁₀ f g = a (section)
+4. β : isSection₀₁ h f = a (retraction))
 
--- Consider SIP
--- Need to ask how they define theorems
+f_hom: ∀ (x y : A), Identity (f (m x y)) (n (f x) (f y)) (homomorphism property)
 
--- Maybe use this?
--- hott0 def isEquiv₀₀_v2 {A B : Type} (f : A → B) : Type :=
---   Σ (g : B → A),
---     Σ (_ : ∀ (a : A), Identity (g (f a)) a),  -- section
---       ∀ (b : B), Identity (f (g b)) b         -- retraction (for same g!)
+Then we prove M = N, which is (A, m) = (B, n)
+
+
+Step 1: Get the carriers equal using set-univalence
+ we can convert the equivalence e into a path p : Identity A B
+ This uses the inverse of the univalence equivalence for sets
+ p = (setUv₀₀ A_set B_set).1 ⟨f, e⟩
+
+Step 2: Transport the operation m along p to get an operation on B
+ transported_op M N M_set N_set e : B → B → B
+
+Step 3: Show that the transported operation is equal to n pointwise
+  For all x,y : B, we have a path
+  Identity (transported_op M N M_set N_set e x y) (N.op x y)
+
+Step 4: Use function extensionality to get the operations equal
+  funext₀ on the pointwise equalities to get
+  Identity (transported_op M N M_set N_set e) (N.op)
+
+Step 5: Combine the equalities of the carriers and operations to get
+  Identity M N
+  using Sigma.eq
+-/
+
+hott0 def magma_equiv (M N : magma) : Type :=
+  Σ (f : M.carrier → N.carrier),
+    Σ (e : isEquiv₀₀ f),
+      ∀ (x y : M.carrier), Identity (f (M.op x y)) (N.op (f x) (f y))
 
 hott0
   axiom equiv_retraction {A B : Type}
@@ -224,60 +238,6 @@ hott0
       (f : A → B) (e : isEquiv₀₀ f) (b : B) :
     Identity (f (e.1 b)) b
 
--- Has let's but cleaner
--- hott0 def magma_eq_of_equiv
---     (M N : magma)
---     (M_set : isSet₀ M.carrier)
---     (N_set : isSet₀ N.carrier)
---     (e : magma_equiv M N)
---     : Identity M N :=
---   -- Steps
---   -- Extract carrier equivalence (both types and operations are equiv/iso)
---   let f := e.1
---   let f_equiv := e.2.1
---   let f_hom := e.2.2
---   let g := f_equiv.1
---   let h := f_equiv.2.1
---   let α := f_equiv.2.2.1
---   let β := f_equiv.2.2.2
-
---   let carrier_eq := (setUv₀₀ M_set N_set).1 ⟨f, f_equiv⟩
-
---   let op_eq : Identity (@Identity.rec Type M.carrier (fun X _ => X → X → X)
---   M.op N.carrier carrier_eq) N.op :=
---       funext₀ (fun x => funext₀ (fun y =>
---         -- Proof chain:
---         -- 1. tranported_op x y = f(M.op(g x, g y)) [by transport_op]
---         -- 2. f(M.op(g x, g y)) = N.op(f(g x), f(g y)) [by f_hom]
---         -- 3. N.op(f(g x), f(g y)) = N.op(x,y) [by β (retraction)]
---     let step1 : Identity
---         (@Identity.rec Type M.carrier (fun X _ => X → X → X)
---           M.op N.carrier carrier_eq x y)
---         (f (M.op (g x) (g y))) :=
---       transport_op M_set N_set f f_equiv M.op x y
-
---     let step2 : Identity
---         (f (M.op (g x) (g y)))
---         (N.op (f (g x)) (f (g y))) :=
---       f_hom (g x) (g y)
-
---     let step3 : Identity
---         (N.op (f (g x)) (f (g y)))
---         (N.op x y) :=
---       ap₂ N.op
---         (equiv_retraction M_set N_set f f_equiv x)
---         (equiv_retraction M_set N_set f f_equiv y)
---     -- Finally, combine to get full equality of magmas
---     step1.trans₀ (step2.trans₀ step3)
---     ))
---   -- Simply combine the two equalities into a Sigma equality to finish
---   Sigma.eq₁ carrier_eq op_eq
-
--- What makes something exactly a def
--- Why should we use def vs theorem??
-
--- Without let's but not as clean
--- Helper definitions to break up the complexity
 set_option maxHeartbeats 5000000
 
 hott0 def magma_carrier_eq
@@ -305,9 +265,9 @@ hott0 def magma_op_eq_pointwise
     (e : magma_equiv M N)
     (x y : N.carrier)
     : Identity (transported_op M N M_set N_set e x y) (N.op x y) :=
-    -- sorry -- this keeps timing out
-  (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
-    ((e.2.2 (e.2.1.1 x) (e.2.1.1 y)).trans₀
-      (ap₂ N.op
-        (equiv_retraction M_set N_set e.1 e.2.1 x)
-        (equiv_retraction M_set N_set e.1 e.2.1 y)))
+    sorry -- this keeps timing out
+  -- (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
+  --   ((e.2.2 (e.2.1.1 x) (e.2.1.1 y)).trans₀
+  --     (ap₂ N.op
+  --       (equiv_retraction M_set N_set e.1 e.2.1 x)
+  --       (equiv_retraction M_set N_set e.1 e.2.1 y)))

From cbfdd318f20fc0a5b81f4d7013ff7713415b721d Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Wed, 28 Jan 2026 20:38:06 -0500
Subject: [PATCH 12/18] Added my current work

---
 test/hott0.lean | 26 +++++++++++++++++---------
 1 file changed, 17 insertions(+), 9 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index b9ea456e..1b3af45c 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -9,6 +9,8 @@ namespace HoTT0
 hott0 def isSection₀₀ {A B : Type} (f : A → B) (g : B → A) : Type :=
   ∀ (a : A), Identity (g (f a)) a
 
+-- Which inverse am I going to use
+-- Consider isContr
 hott0 def isEquiv₀₀ {A B : Type} (f : A → B) : Type :=
   Σ (g : B → A),
     Σ (h : B → A),
@@ -215,7 +217,7 @@ Step 1: Get the carriers equal using set-univalence
  p = (setUv₀₀ A_set B_set).1 ⟨f, e⟩
 
 Step 2: Transport the operation m along p to get an operation on B
- transported_op M N M_set N_set e : B → B → B
+ transported_op M N M_set N_set (e : B → B → B)
 
 Step 3: Show that the transported operation is equal to n pointwise
   For all x,y : B, we have a path
@@ -248,7 +250,7 @@ hott0 def magma_carrier_eq
     (M_set : isSet₀ M.carrier)
     (N_set : isSet₀ N.carrier)
     (e : magma_equiv M N)
-    : Identity M.carrier N.carrier :=
+    : Identity M.carrier N.carrier := -- sorry
   (setUv₀₀ M_set N_set).1 ⟨e.1, e.2.1⟩
 
 -- Try a simpler intermediate definition
@@ -259,8 +261,11 @@ hott0 def transported_op
     (e : magma_equiv M N)
     : N.carrier → N.carrier → N.carrier :=
   @Identity.rec Type M.carrier (fun X _ => X → X → X)
-    M.op N.carrier (magma_carrier_eq M N M_set N_set e)
+    M.op N.carrier ((setUv₀₀ M_set N_set).1 ⟨e.1, e.2.1⟩)
 
+-- TODO : Pointwise Equality SUUUCKS
+-- Implement transported-op the way that was done in Agda
+-- Consider Equiv-elim
 hott0 def magma_op_eq_pointwise
     (M N : magma)
     (M_set : isSet₀ M.carrier)
@@ -268,9 +273,12 @@ hott0 def magma_op_eq_pointwise
     (e : magma_equiv M N)
     (x y : N.carrier)
     : Identity (transported_op M N M_set N_set e x y) (N.op x y) :=
-    sorry -- this keeps timing out
-  -- (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
-  --   ((e.2.2 (e.2.1.1 x) (e.2.1.1 y)).trans₀
-  --     (ap₂ N.op
-  --       (equiv_retraction M_set N_set e.1 e.2.1 x)
-  --       (equiv_retraction M_set N_set e.1 e.2.1 y)))
+  --  sorry -- this keeps timing out
+  (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
+    ((e.2.2 (e.2.1.1 x) (e.2.1.1 y)).trans₀
+      (ap₂ N.op
+        (equiv_retraction M_set N_set e.1 e.2.1 x)
+        (equiv_retraction M_set N_set e.1 e.2.1 y)))
+
+
+-- Charactarize Path Spaces using Identity Types

From cbe565e8cf60e6ff3df0e4595754f98bfd9b17f3 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Thu, 29 Jan 2026 22:43:44 -0500
Subject: [PATCH 13/18] Useful comments and trying things out

---
 test/hott0.lean | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index 1b3af45c..f7ab12ef 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -52,6 +52,7 @@ hott0 def isEquiv₀₀_transport₀ {A B : Type} (h : Identity A B) : isEquiv
 hott0 def Identity.toEquiv₀₀ {A B : Type} : Identity A B → Σ (f : A → B), isEquiv₀₀ f :=
   fun h => ⟨transport₀ h, isEquiv₀₀_transport₀ h⟩
 
+-- Meeting TODO
 --- Another addition of mine TODO
 --Adding Is Contractible over here
 hott0 def isContr₀ (A : Type) : Type := sorry
@@ -76,6 +77,7 @@ hott0
 --====================================
 -- Path Algebra stuff
 
+-- Consider having type aliases for long subgoals
 -- ap on one type
 hott0 def ap {A B : Type} (f : A → B) {a a' : A} (p : Identity a a') : Identity (f a) (f a') :=
   p.rec (Identity.rfl₀)
@@ -142,7 +144,7 @@ hott0 def funext₀ {A : Type} {B : A → Type} {f g : (a : A) → B a}
     (h : ∀ (a : A), Identity (f a) (g a)) : Identity f g :=
   (funext₀₀ f g).1 h
 
----================================
+---====================================
 -- Univalence computation rule
 
 hott0
@@ -202,7 +204,7 @@ with forward map f : A → B and inverse map g : B → A
 
 We have e : isEquiv₀₀ f which gives us:
 1. g : B → A (inverse)
-2. h : B → A (another inver)
+2. h : B → A (another inverse)
 3. α : isSection₁₀ f g = a (section)
 4. β : isSection₀₁ h f = a (retraction))
 
@@ -245,6 +247,7 @@ hott0
 
 set_option maxHeartbeats 5000000
 
+-- Seems to be a problem, maybe try specifying which path to take
 hott0 def magma_carrier_eq
     (M N : magma)
     (M_set : isSet₀ M.carrier)
@@ -266,6 +269,8 @@ hott0 def transported_op
 -- TODO : Pointwise Equality SUUUCKS
 -- Implement transported-op the way that was done in Agda
 -- Consider Equiv-elim
+
+-- Univalence axiom doesn't specify, but asserts existence of a path.
 hott0 def magma_op_eq_pointwise
     (M N : magma)
     (M_set : isSet₀ M.carrier)
@@ -282,3 +287,4 @@ hott0 def magma_op_eq_pointwise
 
 
 -- Charactarize Path Spaces using Identity Types
+-- Unfiolding is crazy

From dd54a601f7282740f3a388425c9331b5da6ff3da Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Thu, 5 Feb 2026 07:51:52 -0500
Subject: [PATCH 14/18] OK builds overnight

---
 test/hott0.lean | 25 ++++++++++++++++++++-----
 1 file changed, 20 insertions(+), 5 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index f7ab12ef..d99e6ad6 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -245,7 +245,7 @@ hott0
       (f : A → B) (e : isEquiv₀₀ f) (b : B) :
     Identity (f (e.1 b)) b
 
-set_option maxHeartbeats 5000000
+set_option maxHeartbeats 500000000
 
 -- Seems to be a problem, maybe try specifying which path to take
 hott0 def magma_carrier_eq
@@ -256,6 +256,7 @@ hott0 def magma_carrier_eq
     : Identity M.carrier N.carrier := -- sorry
   (setUv₀₀ M_set N_set).1 ⟨e.1, e.2.1⟩
 
+-- Strategy Show any two operations on M, or N are the same under univalence
 -- Try a simpler intermediate definition
 hott0 def transported_op
     (M N : magma)
@@ -271,20 +272,34 @@ hott0 def transported_op
 -- Consider Equiv-elim
 
 -- Univalence axiom doesn't specify, but asserts existence of a path.
-hott0 def magma_op_eq_pointwise
+set_option diagnostics true
+
+hott0 def subexpr
     (M N : magma)
     (M_set : isSet₀ M.carrier)
     (N_set : isSet₀ N.carrier)
     (e : magma_equiv M N)
     (x y : N.carrier)
-    : Identity (transported_op M N M_set N_set e x y) (N.op x y) :=
-  --  sorry -- this keeps timing out
-  (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
+    :=
     ((e.2.2 (e.2.1.1 x) (e.2.1.1 y)).trans₀
       (ap₂ N.op
         (equiv_retraction M_set N_set e.1 e.2.1 x)
         (equiv_retraction M_set N_set e.1 e.2.1 y)))
 
 
+hott0 def magma_op_eq_pointwise
+    (M N : magma)
+    (M_set : isSet₀ M.carrier)
+    (N_set : isSet₀ N.carrier)
+    (e : magma_equiv M N)
+    (x y : N.carrier)
+    : Identity (transported_op M N M_set N_set e x y) (N.op x y) :=
+  --  sorry -- this keeps timing out
+  (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
+    (subexpr M N M_set N_set e x y)
+
+
+
+
 -- Charactarize Path Spaces using Identity Types
 -- Unfiolding is crazy

From 9533cf832c8517075d4fd0a2218c961166b5f770 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Thu, 5 Feb 2026 17:24:00 -0500
Subject: [PATCH 15/18] I need to profile this AAAAARGH Stack overflow

---
 test/hott0.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index d99e6ad6..f4f1ebd5 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -300,6 +300,6 @@ hott0 def magma_op_eq_pointwise
 
 
 
-
+-- Profile this thing
 -- Charactarize Path Spaces using Identity Types
 -- Unfiolding is crazy

From 4f0838ae7be163ff3898f5d8ab6423c32bf46f58 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Sat, 14 Mar 2026 19:06:50 -0400
Subject: [PATCH 16/18] Cleaned Up to make pull request

---
 test/hott0.lean | 47 ++++++++++-------------------------------------
 1 file changed, 10 insertions(+), 37 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index f4f1ebd5..5a1a44c7 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -1,16 +1,17 @@
 import HoTTLean.Frontend.Commands
 
+set_option profiler true
+
 noncomputable section
 
 declare_theory hott0
 
 namespace HoTT0
 
+
 hott0 def isSection₀₀ {A B : Type} (f : A → B) (g : B → A) : Type :=
   ∀ (a : A), Identity (g (f a)) a
 
--- Which inverse am I going to use
--- Consider isContr
 hott0 def isEquiv₀₀ {A B : Type} (f : A → B) : Type :=
   Σ (g : B → A),
     Σ (h : B → A),
@@ -52,10 +53,8 @@ hott0 def isEquiv₀₀_transport₀ {A B : Type} (h : Identity A B) : isEquiv
 hott0 def Identity.toEquiv₀₀ {A B : Type} : Identity A B → Σ (f : A → B), isEquiv₀₀ f :=
   fun h => ⟨transport₀ h, isEquiv₀₀_transport₀ h⟩
 
--- Meeting TODO
---- Another addition of mine TODO
 --Adding Is Contractible over here
-hott0 def isContr₀ (A : Type) : Type := sorry
+hott0 def isContr₀ (A : Type) : Type := Σ (a : A), (∀ (b : A), Identity a b)
 
 hott0
   /-- The type `A` is (-1)-truncated. -/
@@ -73,10 +72,6 @@ hott0
     isEquiv₁₀ (@Identity.toEquiv₀₀ A B)
 
 
--- My stuff starts here
---====================================
--- Path Algebra stuff
-
 -- Consider having type aliases for long subgoals
 -- ap on one type
 hott0 def ap {A B : Type} (f : A → B) {a a' : A} (p : Identity a a') : Identity (f a) (f a') :=
@@ -95,7 +90,7 @@ hott0 def Sigma.eta {A : Type} {B : A → Type} (w : Σ (a : A), B a) :
     Identity w ⟨w.1, w.2⟩ := Identity.rfl₀
 
 
--- Well this was a bloody nightmare to figure out
+-- Sigma eq for Type
 hott0 def Sigma.eq {A : Type} {B : A → Type} {w w' : Σ (a : A), B a}
     (p : Identity w.1 w'.1)
     (q : Identity (p.rec w.2) w'.2)
@@ -139,24 +134,11 @@ hott0 def Sigma.eq₁ {A : Type 1} {B : A → Type} {w w' : Σ (a : A), B a}
     w'.2
     q
 
--- hott0 is a custom elaborator that enforces single-definitions
+-- function extensionality
 hott0 def funext₀ {A : Type} {B : A → Type} {f g : (a : A) → B a}
     (h : ∀ (a : A), Identity (f a) (g a)) : Identity f g :=
   (funext₀₀ f g).1 h
 
----====================================
--- Univalence computation rule
-
-hott0
-  /-- Univalence Computation Rule.
-      See HoTT book (Univalent Foundations), Axiom 2.10.3, Remark 2.10.4.
-  -/
-  axiom ua_comp₀₀ {A B : Type}
-    (A_set : isSet₀ A) (B_set : isSet₀ B) (f : A → B) (e : isEquiv₀₀ f) (a : A):
-    --let ⟨ua_inv, _, _, _⟩ := (setUv₀₀ A_set B_set).1
-    Identity (transport₀ ((setUv₀₀ A_set B_set).1 ⟨f, e⟩) a) (f a)
-
-
 --=====================================
 -- Transport on Π-Types
 
@@ -181,7 +163,6 @@ hott0 def magma.carrier (M : magma) : Type := M.1
  -- The Operation
 hott0 def magma.op (M : magma) : M.carrier → M.carrier → M.carrier := M.2
 
--- Retrying how to solve the pull request for issue
 -- Prove that equivalent magmas consisting of set-data (meaning magmas
 -- (A,A×A→A) s.t. the underlying type A is a set) are equal using set-univalence in test/hott0.lean.
 -- A magma homomorphism preserves the operation
@@ -253,11 +234,11 @@ hott0 def magma_carrier_eq
     (M_set : isSet₀ M.carrier)
     (N_set : isSet₀ N.carrier)
     (e : magma_equiv M N)
-    : Identity M.carrier N.carrier := -- sorry
+    : Identity M.carrier N.carrier :=
   (setUv₀₀ M_set N_set).1 ⟨e.1, e.2.1⟩
 
 -- Strategy Show any two operations on M, or N are the same under univalence
--- Try a simpler intermediate definition
+-- Try a simpler intermediate definition for timeouts
 hott0 def transported_op
     (M N : magma)
     (M_set : isSet₀ M.carrier)
@@ -267,9 +248,6 @@ hott0 def transported_op
   @Identity.rec Type M.carrier (fun X _ => X → X → X)
     M.op N.carrier ((setUv₀₀ M_set N_set).1 ⟨e.1, e.2.1⟩)
 
--- TODO : Pointwise Equality SUUUCKS
--- Implement transported-op the way that was done in Agda
--- Consider Equiv-elim
 
 -- Univalence axiom doesn't specify, but asserts existence of a path.
 set_option diagnostics true
@@ -287,6 +265,8 @@ hott0 def subexpr
         (equiv_retraction M_set N_set e.1 e.2.1 y)))
 
 
+-- VEERRY Sloow, give it 1h 15 mins on a MacBook Air with Apple M4, 16GB RAM
+-- With nothing else but VSCode Open
 hott0 def magma_op_eq_pointwise
     (M N : magma)
     (M_set : isSet₀ M.carrier)
@@ -294,12 +274,5 @@ hott0 def magma_op_eq_pointwise
     (e : magma_equiv M N)
     (x y : N.carrier)
     : Identity (transported_op M N M_set N_set e x y) (N.op x y) :=
-  --  sorry -- this keeps timing out
   (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
     (subexpr M N M_set N_set e x y)
-
-
-
--- Profile this thing
--- Charactarize Path Spaces using Identity Types
--- Unfiolding is crazy

From 30facd588d895a72fdafb937b7292239ae9214d9 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Sat, 14 Mar 2026 20:51:54 -0400
Subject: [PATCH 17/18] Needed to include function extensionality and sigma-eq
 for final steps

---
 test/hott0.lean | 32 ++++++++++++++++++++++++++++++--
 1 file changed, 30 insertions(+), 2 deletions(-)

diff --git a/test/hott0.lean b/test/hott0.lean
index 5a1a44c7..2746a72a 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -200,19 +200,24 @@ Step 1: Get the carriers equal using set-univalence
  p = (setUv₀₀ A_set B_set).1 ⟨f, e⟩
 
 Step 2: Transport the operation m along p to get an operation on B
- transported_op M N M_set N_set (e : B → B → B)
+ tranport^{X ↦ X → X → X}(p,m) : B → B → B
 
 Step 3: Show that the transported operation is equal to n pointwise
   For all x,y : B, we have a path
   Identity (transported_op M N M_set N_set e x y) (N.op x y)
 
+  transported_op m x y
+    = f(m(g(x), g(y)))    -- by transport_op
+    = n(f(g(x)), f(g(y))) -- by f_hom
+    = n(x,y)              -- by α (section : f(g(y)) = y) applied twice
+
 Step 4: Use function extensionality to get the operations equal
   funext₀ on the pointwise equalities to get
   Identity (transported_op M N M_set N_set e) (N.op)
 
 Step 5: Combine the equalities of the carriers and operations to get
   Identity M N
-  using Sigma.eq
+
 -/
 
 hott0 def magma_equiv (M N : magma) : Type :=
@@ -259,6 +264,7 @@ hott0 def subexpr
     (e : magma_equiv M N)
     (x y : N.carrier)
     :=
+    -- sorry
     ((e.2.2 (e.2.1.1 x) (e.2.1.1 y)).trans₀
       (ap₂ N.op
         (equiv_retraction M_set N_set e.1 e.2.1 x)
@@ -274,5 +280,27 @@ hott0 def magma_op_eq_pointwise
     (e : magma_equiv M N)
     (x y : N.carrier)
     : Identity (transported_op M N M_set N_set e x y) (N.op x y) :=
+      -- sorry
   (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
     (subexpr M N M_set N_set e x y)
+
+-- Apply function extensionality twice
+hott0 def magma_op_eq
+    (M N : magma)
+    (M_set : isSet₀ M.carrier)
+    (N_set : isSet₀ N.carrier)
+    (e : magma_equiv M N)
+    : Identity (transported_op M N M_set N_set e) N.op :=
+  funext₀ (fun x => funext₀ (fun y =>
+    magma_op_eq_pointwise M N M_set N_set e x y))
+
+-- Combine everything with Sigma.eq
+hott0 def magma_eq_of_equiv
+    (M N : magma)
+    (M_set : isSet₀ M.carrier)
+    (N_set : isSet₀ N.carrier)
+    (e : magma_equiv M N)
+    : Identity M N :=
+  Sigma.eq₁
+    (magma_carrier_eq M N M_set N_set e)
+    (magma_op_eq M N M_set N_set e)

From 0acccd6923bf502854ff936ab84f0376ff86eed7 Mon Sep 17 00:00:00 2001
From: Pesara Amarasekera <2010pesara@gmail.com>
Date: Sat, 14 Mar 2026 22:20:58 -0400
Subject: [PATCH 18/18] Added comments on sorry's for perf debugging

---
 test/hott0.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/hott0.lean b/test/hott0.lean
index 2746a72a..c7650d99 100644
--- a/test/hott0.lean
+++ b/test/hott0.lean
@@ -255,6 +255,7 @@ hott0 def transported_op
 
 
 -- Univalence axiom doesn't specify, but asserts existence of a path.
+-- Left sorry's in, just in case things people want to run it without waiting so long
 set_option diagnostics true
 
 hott0 def subexpr