From 428aaff95da203f90ded78f57a9a1287beddd23c Mon Sep 17 00:00:00 2001 From: 5HT Date: Tue, 31 Oct 2023 02:15:22 +0200 Subject: [PATCH] equiv --- lib/foundations/univalent/equiv.anders | 46 ++++++++++++++------------ lib/foundations/univalent/iso.anders | 4 +-- 2 files changed, 26 insertions(+), 24 deletions(-) diff --git a/lib/foundations/univalent/equiv.anders b/lib/foundations/univalent/equiv.anders index dbdf823..deeb073 100644 --- a/lib/foundations/univalent/equiv.anders +++ b/lib/foundations/univalent/equiv.anders @@ -51,13 +51,32 @@ def univ-computation (A B : U) (p : PathP (<_> U) A B) := Glue B (j ∨ ∂ i) [(i = 0) → (A, univ-elim A B p), (i = 1) → (B, idEquiv B), (j = 1) → (p @ i, univ-elim (p @ i) B ( p @ (i ∨ k)))] +--- Glue Primitive [CCHM] 2016 + +def Glue' (A : U) (φ : I) (e : Partial (Σ (T : U), equiv T A) φ) : U := Glue A φ e +def glue' (A : U) (φ : I) (u : Partial (Σ (T : U), equiv T A × T) φ) + (a : A[φ ↦ [(φ = 1) → (u 1=1).2.1.1 (u 1=1).2.2]]) := glue φ u (ouc a) +def unglue' (A : U) (φ : I) (e : Partial (Σ (T : U), equiv T A) φ) + (a : Glue A φ e) : A := unglue φ e a +def hcomp-Glue' (A : U) (φ : I) + (e : Partial (Σ (T : U), equiv T A) φ) + (ψ : I) (u : I → Partial (Glue A φ [(φ = 1) → e 1=1]) ψ) + (u₀ : (Glue A φ [(φ = 1) → e 1=1])[ψ ↦ u 0]) : Glue A φ [(φ = 1) → e 1=1] + := hcomp (Glue A φ [(φ = 1) → e 1=1]) ψ + (λ (i : I), [(ψ = 1) → u i 1=1]) (ouc u₀) +--- def Glue-computation +--- def Glue-uniqueness + --- Equiv as [Right] Identity System [Escardó] 2014 option girard true def single (B : U) : U := Σ (A: U), equiv A B -def idEquiv≡ (A : U) (y : single A) : Path (single A) (A, idEquiv A) y := ? -def unglueEquiv (A : U) (φ : I) (f : Partial (single A) φ) : equiv (Glue A φ f) A := ? +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) := ? +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 +--- := (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) def isContr→isProp (A: U) (w: isContr A) (a b : A) : Path A a b := hcomp A (∂ i) (λ (j : I), [(i = 0) → a, (i = 1) → (w.2 b) @ j]) (( w.2 a @ -i) @ i) @@ -77,23 +96,9 @@ def ua-β (A B : U) (e : equiv A B) : Path (A → B) (trans A B ((ua A B) e)) e. := λ (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) ---- Glue Primitive [CCHM] 2016 - -def Glue' (A : U) (φ : I) (e : Partial (Σ (T : U), equiv T A) φ) : U := Glue A φ e -def glue' (A : U) (φ : I) (u : Partial (Σ (T : U), equiv T A × T) φ) - (a : A[φ ↦ [(φ = 1) → (u 1=1).2.1.1 (u 1=1).2.2]]) := glue φ u (ouc a) -def unglue' (A : U) (φ : I) (e : Partial (Σ (T : U), equiv T A) φ) - (a : Glue A φ e) : A := unglue φ e a -def hcomp-Glue' (A : U) (φ : I) - (e : Partial (Σ (T : U), equiv T A) φ) - (ψ : I) (u : I → Partial (Glue A φ [(φ = 1) → e 1=1]) ψ) - (u₀ : (Glue A φ [(φ = 1) → e 1=1])[ψ ↦ u 0]) : Glue A φ [(φ = 1) → e 1=1] - := hcomp (Glue A φ [(φ = 1) → e 1=1]) ψ - (λ (i : I), [(ψ = 1) → u i 1=1]) (ouc u₀) ---- def Glue-computation ---- def Glue-uniqueness --- The Half-adjoint equivalence from Homotopy Theory +--- as if f anf g are adjoint functors. def τ (A B : U) (f : A → B) (g : B → A) (η: Path (idᵀ A) (∘ A B A g f) (id A)) @@ -115,15 +120,12 @@ def isHae' (A B : U) (f : A → B): U := (η: 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] +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 diff --git a/lib/foundations/univalent/iso.anders b/lib/foundations/univalent/iso.anders index 16dbbea..2ca4c25 100644 --- a/lib/foundations/univalent/iso.anders +++ b/lib/foundations/univalent/iso.anders @@ -73,14 +73,14 @@ 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 ( s y @ -i) z.2) --- [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 +-- [Cohen, Coquand, Huber, Mörtberg, Joyal] 2016 + 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)