accept П

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

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

lib/foundations/univalent/equiv.anders

@@ -5,15 +5,15 @@
    — 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 -}
 
 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 := <i> (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 := <i> ((w.2 (w.1 x)).2 (x, <j> 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), <i> Glue B (∂ i) [(i = 0) → (A, e), (i = 1) → (B, idEquiv B)]
@@ -39,30 +39,27 @@ def univ-computation (A B : U) (p : PathP (<_> U) A B) : PathP (<_> PathP (<_> U
  := <j i> 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 (<k> 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 (<i> 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
  := <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) : 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
  := <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)
 
-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

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ᵂ *)