From f8a122100d27179a596e2c3634ded63466175d37 Mon Sep 17 00:00:00 2001 From: 5HT Date: Mon, 23 Oct 2023 07:08:17 +0300 Subject: [PATCH] =?UTF-8?q?accept=20=D0=9F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- dune | 6 +----- lib/foundations/mltt/pi.anders | 14 +++++++------- lib/foundations/univalent/equiv.anders | 25 ++++++++++++------------- src/frontend/lexer.mll | 2 +- 4 files changed, 21 insertions(+), 26 deletions(-) diff --git a/dune b/dune index 2786d988..501b341a 100644 --- a/dune +++ b/dune @@ -7,7 +7,6 @@ lib/foundations/mltt/pi.anders lib/foundations/mltt/sigma.anders lib/foundations/univalent/path.anders - lib/foundations/univalent/prop.anders lib/foundations/univalent/equiv.anders lib/foundations/univalent/iso.anders lib/foundations/modal/infinitesimal.anders @@ -17,10 +16,7 @@ lib/mathematics/categories/functor.anders lib/mathematics/categories/abelian.anders lib/mathematics/categories/groupoid.anders - lib/mathematics/topoi/topos.anders - lib/mathematics/meta/favonia.anders - lib/mathematics/meta/awodey.anders - lib/mathematics/meta/kraus.anders + lib/mathematics/categories/topos.anders lib/mathematics/geometry/bundle.anders lib/mathematics/geometry/etale.anders lib/mathematics/geometry/formalDisc.anders diff --git a/lib/foundations/mltt/pi.anders b/lib/foundations/mltt/pi.anders index 2254bfff..7aa37073 100644 --- a/lib/foundations/mltt/pi.anders +++ b/lib/foundations/mltt/pi.anders @@ -9,11 +9,11 @@ module pi where import lib/foundations/univalent/path def Pi (A : U) (B : A → U) : U := Π (x : A), B x -def lambda (A: U) (B: A → U) (b: Pi A B) : Pi A B := λ (x : A), b x -def lam (A B: U) (f: A → B) : A → B ≔ λ (x : A), f x -def apply (A: U) (B: A → U) (f: Pi A B) (a: A) : B a := f a +def Fun (A B: U) : U := П (x : A), B +def lam (A B: U) (f: A → B) : Fun A B ≔ λ (x : A), f x def app (A B: U) (f: A → B) (x: A): B := f x -def Π-β (A : U) (B : A → U) (a : A) (f : Pi A B) - : Path (B a) (apply A B (lambda A B f) a) (f a) := idp (B a) (f a) -def Π-η (A : U) (B : A → U) (a : A) (f : Pi A B) - : Path (Pi A B) f (λ (x : A), f x) := idp (Pi A B) f +def П-lambda (A: U) (B: A → U) (b: Pi A B) : Pi A B := λ (x : A), b x +def П-apply (A: U) (B: A → U) (f: Pi A B) (a: A) : B a := f a +def П-β (A : U) (B : A → U) (a : A) (f : Pi A B) : Path (B a) (П-apply A B (П-lambda A B f) a) (f a) := idp (B a) (f a) +def П-η (A : U) (B : A → U) (a : A) (f : Pi A B) : Path (Pi A B) f (λ (x : A), f x) := idp (Pi A B) f +def П-ind (A : U) (B : A -> U) (C : Pi A B → U) (g: Π (x: Pi A B), C x) : П (p: Pi A B), C p := \ (p: Pi A B), g p diff --git a/lib/foundations/univalent/equiv.anders b/lib/foundations/univalent/equiv.anders index 5cf87557..b72aef11 100644 --- a/lib/foundations/univalent/equiv.anders +++ b/lib/foundations/univalent/equiv.anders @@ -5,7 +5,7 @@ — Surjective, Injective, Embedding, Hae; — Univalence. — Theorems, Gluing; - Copyright (c) Groupoid Infinity, 2014-2022. + Copyright (c) Groupoid Infinity, 2014-2023. HoTT 4.6 Surjections and Embedding -} @@ -13,7 +13,7 @@ module equiv where import lib/foundations/univalent/path option girard true ---- [Pelayo, Warren, Voevodsky] 2012 +--- [Pelayo, Warren] 2012 def fiber (A : U) (B: U) (f: A → B) (y : B) : U := Σ (x : A), Path B y (f x) def isEquiv (A B : U) (f : A → B) : U := Π (y : B), isContr (fiber A B f y) @@ -30,7 +30,7 @@ def inv-equiv (A B : U) (w : equiv A B) : B → A := λ (y : B), (w.2 y).1.1 def ret-equiv (A B : U) (w : equiv A B) (y : B) : Path B (w.1 (inv-equiv A B w y)) y := (w.2 y).1.2 @ -i def sec-equiv (A B : U) (w : equiv A B) (x : A) : Path A (inv-equiv A B w (w.1 x)) x := ((w.2 (w.1 x)).2 (x, w.1 x) @ i).1 ---- Univalence Type (Equiv → Path) +--- Univalence Type (Equiv → Path) [Voevodsky] 2014 def univ-formation (A B : U) := equiv A B → PathP (<_> U) A B def univ-intro (A B : U) : univ-formation A B := λ (e : equiv A B), Glue B (∂ i) [(i = 0) → (A, e), (i = 1) → (B, idEquiv B)] @@ -39,10 +39,9 @@ def univ-computation (A B : U) (p : PathP (<_> U) A B) : PathP (<_> PathP (<_> U := 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)))] ---- Equiv as Identity System +--- Equiv as Identity System [Escardó] 2014 -def singl₁ (B : U) := Σ (A: U), equiv A B -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 single (B : U) : U := Σ (A: U), equiv A B def EquivIsContr (B: U) : isContr (Σ (A: U), equiv A B) := ? def isContr→isProp (A: U) (w: isContr A) (a b : A) : Path A a b @@ -50,19 +49,17 @@ def isContr→isProp (A: U) (w: isContr A) (a b : A) : Path A a b def contrSinglEquiv (A B : U) (e : equiv A B) : PathP (<_>Σ(X:U), equiv X B) (B,idEquiv B) (A,e) := isContr→isProp (Σ(A: U),equiv A B) (EquivIsContr B) (B,idEquiv B) (A,e) def J-equiv (A B: U) (P: Π (A: U), equiv A B → U) (r: P B (idEquiv B)) : Π (e: equiv A B), P A e - := λ (e: equiv A B), subst₁ (singl₁ B) (\ (z: singl₁ B), P z.1 z.2) (B,idEquiv B) (A,e) (contrSinglEquiv A B e) r + := λ (e: equiv A B), subst (single B) (\ (z: single B), P z.1 z.2) (B,idEquiv B) (A,e) (contrSinglEquiv A B e) r + +--- [Pitts] 2016 def ua (A B : U) : equiv A B -> PathP (<_> U) A B := \ (p: equiv A B), univ-intro A B p def ua' (A B : U) : PathP (<_> U) A B -> equiv A B := \ (p: PathP (<_>U) A B), univ-elim A B p def ua-β (A B : U) (e : equiv A B) : Path (A → B) (trans A B ((ua A B) e)) e.1 := λ (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) -def isContr₁ (A : U₁) := Σ (x: A), Π (y: A), PathP (<_>A) x y -def fiber₁ (A : U₁) (B: U) (f: A → B) (y : B) : U₁ := Σ (x : A), Path B y (f x) -def isEquiv₁ (A : U₁) (B : U) (f : A → B) : U₁ := Π (y : B), isContr₁ (fiber₁ A B f y) -def ua'-IsEquiv (A B: U) := isEquiv₁ (PathP (<_>U) A B) (equiv A B) (ua' A B) - ---- Primitives +--- 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) φ) @@ -75,3 +72,5 @@ def hcomp-Glue' (A : U) (φ : I) (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 diff --git a/src/frontend/lexer.mll b/src/frontend/lexer.mll index a6d8ddf7..2a1ea194 100644 --- a/src/frontend/lexer.mll +++ b/src/frontend/lexer.mll @@ -78,7 +78,7 @@ rule main = parse match s with | "/\\" | "\xE2\x88\xA7" -> AND (* ∧ *) | "\\/" | "\xE2\x88\xA8" -> OR (* ∨ *) - | "forall" | "\xCE\xA0" -> PI (* Π *) + | "forall" | "\xCE\xA0" | "П" -> PI (* Π *) | "summa" | "\xCE\xA3" -> SIGMA (* Σ *) | "\\" | "\xCE\xBB" -> LAM (* λ *) | "ind-W" | "ind\xE1\xB5\x82" -> INDW (* indᵂ *)