equiv

lib/foundations/univalent/equiv.anders

@@ -73,20 +73,17 @@ option girard true
 
 def single (B : U) : U := Σ (A: U), equiv A B
 def part (A: U) (i : I) (w : single A) : Partial (single A) (-i ∨ i) := [ (i = 0) → (A, idEquiv A), (i = 1) → w ]
-def unglueIsEquiv (A : U) (φ : I) (f : Partial (single A) φ) : isEquiv (Glue A φ f) A (unglue' A φ f) := ?
+axiom unglueIsEquiv (A : U) (φ : I) (f : Partial (single A) φ) : isEquiv (Glue A φ f) A (unglue' A φ f)
 def unglueEquiv (A : U) (φ : I) (f : Partial (single A) φ) : equiv (Glue A φ f) A := (unglue' A φ f, unglueIsEquiv A φ f)
 axiom idEquiv≡ (A : U) (w : single A) : Path (single A) (A, idEquiv A) w
---- := <i> (Glue' A (∂ i) (part A (∂ i) w), unglueEquiv A (∂ i) (part A (∂ i) w))
-def EquivIsContr (B: U) : isContr (single B) := ((B, idEquiv B), idEquiv≡ B)
+-- := <i> (Glue' A (∂ i) (part A (∂ i) w), unglueEquiv A (∂ i) (part A (∂ i) w))
+def EquivIsContr (A: U) : isContr (single A) := ((A, idEquiv A), idEquiv≡ A)
 def isContr→isProp (A: U) (w: isContr A) (a b : A) : Path A a b
  := <i> hcomp A (∂ i) (λ (j : I), [(i = 0) → a, (i = 1) → (w.2 b) @ j]) ((<i4> w.2 a @ -i) @ i)
-def contrSinglEquiv (A B : U) (e : equiv A B)
-  : Path (single B) (B,idEquiv B) (A,e)
+def contrSinglEquiv (A B : U) (e : equiv A B) : Path (single B) (B,idEquiv B) (A,e)
  := isContr→isProp (single B) (EquivIsContr B) (B,idEquiv B) (A,e)
-def J-equiv (A B: U) (P: Π (A B: U), equiv A B → U) (r: P B B (idEquiv B))
-  : Π (e: equiv A B), P A B e
- := λ (e: equiv A B), subst (single B) (\ (z: single B), P z.1 B z.2)
-                            (B,idEquiv B) (A,e) (contrSinglEquiv A B e) r
+def J-equiv (A B: U) (P: Π (A B: U), equiv A B → U) (r: P B B (idEquiv B)) : Π (e: equiv A B), P A B e
+ := λ (e: equiv A B), subst (single B) (\ (z: single B), P z.1 B z.2) (B,idEquiv B) (A,e) (contrSinglEquiv A B e) r
 
 --- [Pitts] 2016
 
@@ -96,7 +93,6 @@ def ua-β (A B : U) (e : equiv A B) : Path (A → B) (trans A B ((ua A B) e)) e.
  := <i> λ (x : A), (idfun=idfun″ B @ -i) ((idfun=idfun″ B @ -i) ((idfun=idfun′ B @ -i) (e.1 x)))
 def ua'-IsEquiv (A B: U) := isEquiv (PathP (<_>U) A B) (equiv A B) (ua' A B)
 
-
 --- The Half-adjoint equivalence from Homotopy Theory
 --- as if f anf g are adjoint functors.
 

lib/foundations/univalent/iso.anders

@@ -103,10 +103,6 @@ def iso-J (A B: U) (P: Π (A B: U), iso A B → U) (r: P B B (iso-intro B))
  := λ (e: iso A B), subst (iso-single B) (\ (z: iso-single B), P z.1 B z.2)
                           (B,iso-intro B) (A,e) (iso-contrSinglEquiv A B e) r
 
--- Similar to Fibrational Equivalence the notion of Retract/Section based Isomorphism could be introduced
--- as forth-back transport between isomorphism and path equality. This notion is somehow cannonical to all
--- cubical systems and is called Unimorphism here.
-
 -- Unimorphism Type (Iso -> Path)
 
 def uni-Form (A B: U) : U₁ := iso A B -> PathP (<_>U) A B

lib/foundations/univalent/path.anders

@@ -155,8 +155,7 @@ def Δ³-3-4 : PathP (<_> Δ³) Δ³-3 Δ³-4 := <i> (i, 1, 1, ref i, ref 1)
 
 def seg : PathP (<_> I) 0 1 := <i> i
 def Partial-app (A : U) (i : I) (u : Partial A i) (p : 1= i) : A := u p
-def Id-path (A : U) (a b : A) : Id A a b → Path A a b
- := idJ A (λ (a b : A) (_ : Id A a b), Path A a b) a (<_> a) b
+def Id-path (A : U) (a b : A) : Id A a b → Path A a b := idJ A (λ (a b : A) (_ : Id A a b), Path A a b) a (<_> a) b
 def Partial' (A : U) (i : I) : V := Partial A i
 def sub (A : U) (i : I) (u : Partial A i) : V := A [i ↦ u]
 def inc′ (A : U) (i : I) (a : A) : sub A i [(i = 1) → a] := inc A i a
@@ -280,8 +279,8 @@ def comp-Path-assoc (A : U) (a b c d : A) (f : Path A a b) (g : Path A b c) (h :
     hcompⁱ (Π (x : A), B) [φ ↦ u] u₀ v = hcompⁱ B(x/v) [φ ↦ u v] (u₀ v)
     hcompⁱ (Σ (x : A), B) [φ ↦ u] u₀ = (v(i/1), compⁱ B(x/v) [φ ↦ u.2] u₀.2), v = hFillⁱ A [φ ↦ u.1] u₀.1
     hcompⁱ (Pathʲ A v w) [φ ↦ u] u₀ = 〈j〉 hcompⁱ A [ φ ↦ u j, (j = 0) ↦ v, (j = 1) ↦ w ] (u₀ j)
-    hcompⁱ G [ψ ↦ u] u₀ = glue [φ ↦ t₁] a₁ : G, G = Glue [φ ↦ (T,w)] A
-           t₁ = u(i/1) : T, a₁ = unglue u(i/1) : A, glue [φ ↦ t₁] a1 = t₁ : T
+    hcompⁱ G [ψ ↦ u] u₀ = glue [φ ↦ t₁] a₁ : G, G = Glue [φ ↦ (T,w)] A, t₁ = u(i/1) : T,
+           a₁ = unglue u(i/1) : A, glue [φ ↦ t₁] a1 = t₁ : T
 
     tFillⁱ A φ u₀ = transpʲ A(i/i∧j) (φ∨(i=0)) u₀ : A
     hFillⁱ A [φ ↦ u] u₀ = hcompʲ A [φ ↦ u(i/i∧j), (i=0) ↦ u₀] u₀ : A
@@ -365,7 +364,7 @@ def transp′′  (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I),
 def transp′′′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := transp (<i> (λ (_ : I), A) i) j
 
 def idfun  (A : U) : A → A := λ (a : A), a
-def idfun′ (A : U) : A → A := transp (<_> A) 0
+def idfun′ (A : U) : A → A := transp (<i> A) 0
 def idfun″ (A : U) : A → A := λ (a : A), hcomp A 0 (λ (i : I), []) a
 
 def idfun=idfun′  (A : U) : Path (A → A) (idfun A)  (idfun′ A) := <i> transp (<_> A) -i