From d89300888b70498f70d0b04e937c62da561a4274 Mon Sep 17 00:00:00 2001 From: 5HT Date: Fri, 20 Oct 2023 21:08:49 +0300 Subject: [PATCH] iso0J --- lib/foundations/univalent/equiv.anders | 4 ++-- lib/foundations/univalent/iso.anders | 17 +++++++++++------ lib/mathematics/geometry/bundle.anders | 2 +- 3 files changed, 14 insertions(+), 9 deletions(-) diff --git a/lib/foundations/univalent/equiv.anders b/lib/foundations/univalent/equiv.anders index 6ee91904..9e49ba97 100644 --- a/lib/foundations/univalent/equiv.anders +++ b/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) := (p @ i, 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) := (p @ i, 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 ( 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 diff --git a/lib/foundations/univalent/iso.anders b/lib/foundations/univalent/iso.anders index cf73224d..c80ee627 100644 --- a/lib/foundations/univalent/iso.anders +++ b/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 ( p @ -i), trans⁻¹-trans A B p, λ (a : A), 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 diff --git a/lib/mathematics/geometry/bundle.anders b/lib/mathematics/geometry/bundle.anders index 44358931..0ced5329 100644 --- a/lib/mathematics/geometry/bundle.anders +++ b/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)