equiv prop

groupoid · Oct 24, 2023 · 521a035 · 521a035
1 parent d399617
commit 521a035
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 14 deletions.
diff --git a/lib/foundations/univalent/equiv.anders b/lib/foundations/univalent/equiv.anders
@@ -1,13 +1,16 @@
 {- Equivalence: https://anders.groupoid.space/foundations/univalent/equiv
    — Fibers;
    — Contractability of Fibers and Singletons;
-   — Equivalence.
+   — Equivalence;
    — Surjective, Injective, Embedding, Hae;
-   — Univalence.
-   — Theorems, Gluing;
-   Copyright (c) Groupoid Infinity, 2014-2023.
+   — Univalence;
+   — Theorems, Gluing.
 
-   HoTT 4.6 Surjections and Embedding -}
+   HoTT 4.2.4 Fiber
+   HoTT 4.6 Surjections and Embedding
+   HoTT 5.8.5 Equivalence Induction
+
+   Copyright (c) Groupoid Infinity, 2014-2023. -}
 
 module equiv where
 import lib/foundations/univalent/path

diff --git a/lib/foundations/univalent/extensionality.anders b/lib/foundations/univalent/extensionality.anders
@@ -1,10 +1,10 @@
 {- FunExt Type: https://anders.groupoid.space/foundations/univalent/funext
-   - Homotopy
-   - Identity System
-   - Function Extensionality
-   - FunExt as Isomorphism
+   — Homotopy;
+   — Identity System;
+   — Function Extensionality;
+   — FunExt as Isomorphism.
 
-   HoTT 2.9 Pi-types and the function extensionality axiom.
+   HoTT 2.9 Pi-types and the function extensionality axiom
 
    Copyright (c) Groupoid Infinity, 2014-2023. -}
 

diff --git a/lib/foundations/univalent/prop.anders b/lib/foundations/univalent/prop.anders
@@ -31,12 +31,19 @@ def propSet (A : U) (h : isProp A) : isSet A
 def lemProp (A : U) (h : A -> isProp A) : isProp A := \(a : A), h a a
 
 def T (A : U) (x : A) : U := Π (y : A), Path A x y
-def lem1 (A : U) (t: isContr A) (x y : A) : Path A x y := comp-Path A x t.1 y (<i> t.2 x @ -i) (t.2 y)
-def lem2 (A : U) (t: isContr A) (x : A) : isProp (T A x) := propPi A (\ (y : A), Path A x y) (propSet A (lem1 A t) x)
 
-def propIsContr (A : U) : isProp (isContr A) := lemProp (isContr A) (\(t: isContr A), propSig A (T A) (lem1 A t) (lem2 A t))
-def propIsProp (A : U) : isProp (isProp A) := \(f g : isProp A), <i> \(a b : A), propSet A f a b (f a b) (g a b) @ i
+def lem1 (A : U) (t: isContr A) (x y : A) : Path A x y
+ := comp-Path A x t.1 y (<i> t.2 x @ -i) (t.2 y)
 
+def lem2 (A : U) (t: isContr A) (x : A)
+  : isProp (T A x)
+ := propPi A (\ (y : A), Path A x y) (propSet A (lem1 A t) x)
+
+def propIsContr (A : U) : isProp (isContr A)
+ := lemProp (isContr A) (\(t: isContr A), propSig A (T A) (lem1 A t) (lem2 A t))
+
+def propIsProp (A : U) : isProp (isProp A)
+ := \(f g : isProp A), <i> \(a b : A), propSet A f a b (f a b) (g a b) @ i
 
 def corSigProp (A: U) (B: A -> U) (pB : Π (x:A), isProp (B x)) (t u : Σ(x:A), B x) (p:PathP (<_>A) t.1 u.1)
   : isProp (PathP (<i>B (p @ i)) t.2 u.2)