From 8fb5af00625c02b9ad28fb2f0fb54a48f1fe7269 Mon Sep 17 00:00:00 2001
From: 5HT <maxim@synrc.com>
Date: Tue, 31 Oct 2023 00:47:24 +0200
Subject: [PATCH] iso

---
 lib/foundations/univalent/equiv.anders | 44 +++++++++++++++++++++-----
 lib/foundations/univalent/iso.anders   | 15 ++++-----
 lib/foundations/univalent/path.anders  |  1 +
 3 files changed, 44 insertions(+), 16 deletions(-)

diff --git a/lib/foundations/univalent/equiv.anders b/lib/foundations/univalent/equiv.anders
index e35d3125..dbdf823f 100644
--- a/lib/foundations/univalent/equiv.anders
+++ b/lib/foundations/univalent/equiv.anders
@@ -2,13 +2,16 @@
    — Fibers;
    — Contractability of Fibers and Singletons;
    — Equivalence;
-   — Surjective, Injective, Embedding
-   - Half-adjoint equivalence;
+   — Surjective, Injective, Embedding;
+   — Half-adjoint equivalence;
+   — Bi-invertible;
    — Univalence;
    — Theorems, Gluing.
 
    HoTT 2.10 Universes and univalence axiom
+   HoTT 4.2 Half-adjoint equivalence
    HoTT 4.2.4 Fiber
+   HoTT 4.3 Bi-invertible maps
    HoTT 4.4 Contractible Fibers
    HoTT 4.6 Surjections and Embedding
    HoTT 5.8.5 Equivalence Induction
@@ -90,12 +93,37 @@ def hcomp-Glue' (A : U) (φ : I)
 --- def Glue-computation
 --- def Glue-uniqueness
 
--- The other notion of equality such as Half Adjoint Equivalence and
--- Bi-Invertible Equivalences could be introduced and encoded as isomorphism by analogy.
+--- The Half-adjoint equivalence from Homotopy Theory
 
-def isHae (A B : U) (f : A -> B): U :=
-  Σ (g : B -> A) (eta_: Path (idᵀ A) (∘ A B A g f) (id A)) (eps_: Path (idᵀ B) (∘ B A B f g) (id B)),
-  Π (x : A), Path B (f ((eta_ @ 0) x)) ((eps_ @ 0) (f x))
+def τ (A B : U) (f : A → B) (g : B → A)
+    (η: Path (idᵀ A) (∘ A B A g f) (id A))
+    (ε: Path (idᵀ B) (∘ B A B f g) (id B)) : U
+ := Π (x : A), Path B (f ((η @ 0) x)) ((ε @ 0) (f x))
 
-def hae (A B : U) : U := Σ (f : A -> B), isHae A B f
+def ν (A B : U) (f : A → B) (g : B → A)
+    (η: Path (idᵀ A) (∘ A B A g f) (id A))
+    (ε: Path (idᵀ B) (∘ B A B f g) (id B)) : U
+ := Π (y : B), Path A (g ((ε @ 0) y)) ((η @ 0) (g y))
+
+def isHae (A B : U) (f : A → B): U :=
+  Σ (g : B → A)
+    (η: Path (idᵀ A) (∘ A B A g f) (id A))
+    (ε: Path (idᵀ B) (∘ B A B f g) (id B)), τ A B f g η ε
+
+def isHae' (A B : U) (f : A → B): U :=
+  Σ (g : B → A)
+    (η: Path (idᵀ A) (∘ A B A g f) (id A))
+    (ε: Path (idᵀ B) (∘ B A B f g) (id B)), ν A B f g η ε
+
+def isHae=isHae' (A B : U) (f : A → B) : U := Path U (isHae A B f) (isHae' A B f)
+
+def hae (A B : U) : U := Σ (f : A → B), isHae A B f
+
+def isHae'' (A B : U) (f : A → B) : U :=
+  Σ (g : B → A)
+    (linv : Π (a : A), Path A a (g (f a)))
+    (rinv : Π (b : B), Path B b (f (g b))),
+  Π (a: A), Path B (cong A B f a (g (f a)) (linv a) @ 0) (rinv (f a) @ 0)
+
+--- Bi-invertible maps [Joyal]
 
diff --git a/lib/foundations/univalent/iso.anders b/lib/foundations/univalent/iso.anders
index deefd35c..16dbbeae 100644
--- a/lib/foundations/univalent/iso.anders
+++ b/lib/foundations/univalent/iso.anders
@@ -73,14 +73,13 @@ def isoToEquiv (A B : U) (f : A -> B) (g : B -> A)
       \ (z : fiber A B f y),
         lemIso A B f g s t (g y) z.1 y (<i> s y @ -i) z.2)
 
--- [Cohen, Coquand, Huber, Mörtberg] 2016
-
-def iso (A B: U) : U :=
-  Σ (f : A -> B)
-    (g : B -> A)
-    (s : section A B f g)
-    (t : retract A B f g),
-    𝟏
+-- [Cohen, Coquand, Huber, Mörtberg, Joyal] 2016
+
+def isIso (A B: U) (f: A → B) : U := Σ (g : B → A) (s : section A B f g ) (t : retract A B f g ), 𝟏
+def isBiInv (A B: U) (f: A → B) : U := Σ (g₁ g₂ : B → A) (s : section A B f g₁) (t : retract A B f g₂), 𝟏
+
+def iso (A B: U) : U := Σ (f : A → B), isIso A B f
+def biinv (A B: U) : U := Σ (f : A → B), isBiInv A B f
 
 def iso→Path (A B : U) (f : A -> B) (g : B -> A)
     (s : Π (y : B), Path B (f (g y)) y)
diff --git a/lib/foundations/univalent/path.anders b/lib/foundations/univalent/path.anders
index 46c03aeb..c5fc862d 100644
--- a/lib/foundations/univalent/path.anders
+++ b/lib/foundations/univalent/path.anders
@@ -33,6 +33,7 @@ def isContr (A: U) : U := Σ (x: A), Π (y: A), Path A x y
 def isContrSingl (A : U) (a : A) : isContr (singl A a) := ((a,idp A a),(\ (z:singl A a), contr A a z.1 z.2))
 def cong (A B : U) (f : A → B) (a b : A) (p : Path A a b) : Path B (f a) (f b) := <i> f (p @ i)
 def ap (A: U) (a x: A) (B: A → U) (f: A → B a) (b: B a) (p: Path A a x): Path (B a) (f a) (f x) := <i> f (p @ i)
+def mapOnPath (A: U) (B: A → U) (a: A) (f: A → B a) (b: B a) (x: A) (p: Path A a x): Path (B a) (f a) (f x) := <i> f (p @ i)
 def inv (A: U) (a b: A) (p: Path A a b): Path A b a := <i> p @ -i
 def Path-η (A : U) (x y : A) (p : Path A x y) : Path (Path A x y) p (<i> p @ i) := <_> p
 def idp-left (A : U) (x y : A) (p : Path A x y) : Path (Path A x x) (<_> x) (<_> p @ 0) := <_ _> x