iso0J

lib/foundations/univalent/equiv.anders

@@ -41,7 +41,8 @@ def univ-computation (A B : U) (p : PathP (<_> U) A B) : PathP (<_> PathP (<_> U
 --- Nominal Lift to U₁
 
 def singl₁ (A : U₁) (a: A) : U₁ := Σ (x: A), PathP (<_>A) a x
-def contr₁ (A : U) (a b : A) (p : PathP (<_>A) a b) : PathP (<_>Σ (x : A), PathP (<_>A) a x) (a,<_>a) (b,p) := <i> (p @ i, <j> p @ i /\ j)
+def singl₁' (A : U) := Σ (X: U) (f : A → X), isEquiv A X f
+def contr₁ (A : U₁) (a b : A) (p : PathP (<_>A) a b) : PathP (<_>Σ (x : A), PathP (<_>A) a x) (a,<_>a) (b,p) := <i> (p @ i, <j> p @ i /\ j)
 def fiber₁ (A : U₁) (B: U) (f: A → B) (y : B) : U₁ := Σ (x : A), Path B y (f x)
 def subst₁ (A : U₁) (P : A -> U₁) (a b : A) (p : PathP (<_>A) a b) (e : P a) : P b := transp (<i> P (p @ i)) 0 e
 def isContr₁ (A : U₁) := Σ (x: A), Π (y: A), PathP (<_>A) x y
@@ -51,7 +52,6 @@ def isEquiv₁ (A : U₁) (B : U) (f : A → B) : U₁ := Π (y : B), isContr₁
 
 def D-equiv := Π (A B: U), equiv A B → U₁
 axiom J-equiv (A B: U) (C: D-equiv) (d: C A A (idEquiv A)) (p: equiv A B) : C A B p
--- := subst₁ (singl₁ U A) (\ (z: singl₁ U A), C A z.1 z.2) (A,<_>A) (B,p) (contr₁ U A B ((univ-intro A B) p)) d
 
 -- [Orton, Pitts] 2017
 

lib/foundations/univalent/iso.anders

@@ -80,9 +80,14 @@ def iso (A B: U) : U :=
     (s : section A B f g)
     (t : retract A B f g), unit
 
-def iso-inro (A: U) : iso A A := (id A, id A, (\(x:A), <_>x), (\(x:A), <_>x), star)
+def iso-intro (A: U) : iso A A := (id A, id A, (\(x:A), <_>x), (\(x:A), <_>x), star)
 
-def isoPath (A B : U) (f : A -> B) (g : B -> A)
+axiom iso-J (A B: U) (C : Π (A B : U) (f: A → B) (g: B → A), U)
+    (d : C A A (id A) (id A))
+    (f : A → B) (g : B → A) (s: section A B f g) (t: retract A B f g)
+  : C A B f g
+
+def iso→Path (A B : U) (f : A -> B) (g : B -> A)
     (s : Π (y : B), Path B (f (g y)) y)
     (t : Π (x : A), Path A (g (f x)) x)
   : PathP (<_> U) A B
@@ -95,9 +100,9 @@ def isoPath (A B : U) (f : A -> B) (g : B -> A)
 
 -- Unimorphism Type (Iso -> Path)
 
-def iso-Form (A B: U) : U₁ := iso A B -> PathP (<_>U) A B
-def iso-Intro (A B: U) : iso-Form A B := \ (x : iso A B), isoPath A B x.f x.g x.s x.t
-def iso-Elim (A B : U) : PathP (<_> U) A B -> iso A B
+def uni-Form (A B: U) : U₁ := iso A B -> PathP (<_>U) A B
+def uni-Intro (A B: U) : uni-Form A B := \ (x : iso A B), iso→Path A B x.f x.g x.s x.t
+def uni-Elim (A B : U) : PathP (<_> U) A B -> iso A B
  := λ (p : PathP (<_> U) A B), ( coerce A B p, coerce B A (<i> p @ -i), trans⁻¹-trans A B p, λ (a : A), <k> trans-trans⁻¹ A B p a @ -k, star )
 
 -- The notion of Minivalence as forth-back map between fibrational equivalence
@@ -106,7 +111,7 @@ def iso-Elim (A B : U) : PathP (<_> U) A B -> iso A B
 -- Minivalence Type (Iso -> Equiv)
 
 def mini-Form (A B : U) : U := iso A B -> equiv A B
-def mini-Intro (A B : U) : mini-Form A B := \ (x : iso A B), univ-elim A B (isoPath A B x.f x.g x.s x.t)
+def mini-Intro (A B : U) : mini-Form A B := \ (x : iso A B), univ-elim A B (iso→Path A B x.f x.g x.s x.t)
 def mini-Elim (A B : U) : equiv A B -> iso A B := \ (x : equiv A B), ( x.f, inv-equiv A B x, ret-equiv A B x, sec-equiv A B x, star)
 
 -- The other notion of equality such as Half Adjoint Equivalence and

lib/mathematics/geometry/bundle.anders

@@ -36,7 +36,7 @@ def encode-decode-Pi (B : U) (F : B → U) (y : B) (x : fiber (Sigma B F) B (pr
 
 def Bundle=Pi (B : U) (F : B → U) (y : B)
   : PathP (<_> U) (fiber (Sigma B F) B (pr₁ B F) y) (F y)
- := isoPath (fiber (Sigma B F) B (pr₁ B F) y) (F y)
+ := iso→Path (fiber (Sigma B F) B (pr₁ B F) y) (F y)
     (encode-Pi B F y) (decode-Pi B F y)
     (decode-encode-Pi B F y) (encode-decode-Pi B F y)