Merge pull request #136 from TashiWalde/is-rezk-Unit

discrete and contractible types are Rezk

src/simplicial-hott/04-right-orthogonal.rzk.md

@@ -15,7 +15,6 @@ function extensionality:
 #assume naiveextext : NaiveExtExt
 #assume extext : ExtExt
 #assume funext : FunExt
-#assume weakextext : WeakExtExt
 ```
 
 ## Right orthogonal maps with respect to shapes
@@ -948,18 +947,25 @@ Weak extension extensionality says that every contractible type has unique
 extensions for every shape inclusion `ϕ ⊂ ψ`.
 
 ```rzk
-#def has-unique-extensions-is-contr uses (weakextext)
+#def has-unique-extensions-is-contr uses (extext)
   ( C : U)
   ( is-contr-C : is-contr C)
   : has-unique-extensions I ψ ϕ C
   :=
-    weakextext I ψ ϕ
+    weakextext-extext extext I ψ ϕ
     ( \ _ → C) ( \ _ → is-contr-C)
 
-#def has-unique-extensions-Unit uses (weakextext)
+#def is-local-type-is-contr uses (extext)
+  ( C : U)
+  ( is-contr-C : is-contr C)
+  : is-local-type I ψ ϕ C
+  :=
+    is-local-type-has-unique-extensions I ψ ϕ C
+    ( has-unique-extensions-is-contr C is-contr-C)
+
+#def has-unique-extensions-Unit uses (extext)
   : has-unique-extensions I ψ ϕ Unit
   := has-unique-extensions-is-contr Unit is-contr-Unit
-
 ```
 
 Unique extension types are closed under equivalence.
@@ -991,7 +997,7 @@ Unique extension types are closed under equivalence.
 
 Next we prove the logical equivalence between `has-unique-extensions` and
 `is-right-orthogonal-terminal-map`. This follows directly from the fact that
-`Unit` has unique extensions (using `weakextext : WeakExtExt`).
+`Unit` has unique extensions (using `extext`).
 
 ```rzk
 #section is-right-orthogonal-terminal-map
@@ -1001,7 +1007,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
 #variable A : U
 
 #def has-unique-extensions-is-right-orthogonal-terminal-map
-  uses (weakextext)
+  uses (extext)
   ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A)
   : has-unique-extensions I ψ ϕ A
   :=
@@ -1011,7 +1017,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( has-unique-extensions-Unit I ψ ϕ)
 
 #def has-unique-extensions-is-right-orthogonal-a-terminal-map
-  uses (weakextext)
+  uses (extext)
   ( tm : A → Unit)
   ( is-orth-ψ-ϕ-tm : is-right-orthogonal-to-shape I ψ ϕ A Unit tm)
   : has-unique-extensions I ψ ϕ A
@@ -1022,7 +1028,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( has-unique-extensions-Unit I ψ ϕ)
 
 #def is-right-orthogonal-terminal-map-has-unique-extensions
-  uses (weakextext)
+  uses (extext)
   ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
   : is-right-orthogonal-terminal-map I ψ ϕ A
   :=
@@ -1031,15 +1037,15 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( terminal-map A)
 
 #def is-right-orthogonal-terminal-map-is-local-type
-  uses (weakextext)
+  uses (extext)
   ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A)
   : is-right-orthogonal-terminal-map I ψ ϕ A
   :=
     is-right-orthogonal-terminal-map-has-unique-extensions
     ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A)
 
 #def is-local-type-is-right-orthogonal-terminal-map
-  uses (weakextext)
+  uses (extext)
   ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A)
   : is-local-type I ψ ϕ A
   :=
@@ -1059,7 +1065,7 @@ from the unit type.
 
 ```rzk
 #def has-fiberwise-unique-extensions-is-right-orthogonal-to-shape
-  uses (extext weakextext)
+  uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -1084,7 +1090,7 @@ every fiber of every map `α : A' → A` also has unique extensions.
 
 ```rzk
 #def has-fiberwise-unique-extensions-have-unique-extensions
-  uses (extext weakextext)
+  uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -1230,7 +1236,7 @@ implication with respect to types with unique extensions.
 Every anodyne shape inclusion is weak anodyne.
 
 ```rzk
-#def is-weak-anodyne-is-anodyne-for-shape uses (weakextext)
+#def is-weak-anodyne-is-anodyne-for-shape uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1255,7 +1261,7 @@ analog fo weak anodyne shape inclusions.
   := \ _ has-ue₀ → has-ue₀
 
 #def implication-has-unique-extension-implication-right-orthogonal
-  uses (weakextext)
+  uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1277,7 +1283,7 @@ analog fo weak anodyne shape inclusions.
         has-ue-ψ-ϕ))
 
 #def is-weak-anodyne-pushout-product-for-shape
-  uses (naiveextext weakextext)
+  uses (naiveextext extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1298,7 +1304,7 @@ analog fo weak anodyne shape inclusions.
     ( A) (f A has-ue₀)
 
 #def is-weak-anodyne-pushout-product-for-shape'
-  uses (naiveextext weakextext)
+  uses (naiveextext extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )

src/simplicial-hott/05-segal-types.rzk.md

@@ -1940,7 +1940,7 @@ Segal type. This is an instance of a general statement about types with unique
 extensions for the shape inclusion `Λ ⊂ Δ²`.
 
 ```rzk
-#def is-fiberwise-segal-are-segal uses (extext weakextext)
+#def is-fiberwise-segal-are-segal uses (extext)
   ( A B : U)
   ( f : A → B)
   ( is-segal-A : is-segal A)
@@ -1949,8 +1949,7 @@ extensions for the shape inclusion `Λ ⊂ Δ²`.
   : is-segal (fib A B f b)
   :=
     is-segal-has-unique-inner-extensions (fib A B f b)
-    ( has-fiberwise-unique-extensions-have-unique-extensions
-      extext weakextext
+    ( has-fiberwise-unique-extensions-have-unique-extensions extext
       ( 2 × 2) (Δ²) (\ t → Λ t) A B f
       ( has-unique-inner-extensions-is-segal A is-segal-A)
       ( has-unique-inner-extensions-is-segal B is-segal-B)

src/simplicial-hott/07-discrete.rzk.md

@@ -336,6 +336,26 @@ For instance, the arrow type of a discrete type is discrete.
   := is-discrete-extension-type 2 Δ¹ (\ _ → A) (\ _ → is-discrete-A)
 ```
 
+## Contractible types are discrete
+
+Every contractible type is automatically discrete.
+
+```rzk
+#def is-discrete-is-contr uses (extext)
+  ( A : U)
+  : is-contr A → is-discrete A
+  :=
+  \ is-contr-A →
+    ( is-discrete-is-Δ¹-local A
+      ( is-Δ¹-local-is-left-local A
+        ( is-local-type-is-contr extext 2 Δ¹ (\ t → t ≡ 0₂) A
+          is-contr-A)))
+
+#def is-discrete-Unit uses (extext)
+  : is-discrete Unit
+  := is-discrete-is-contr Unit (is-contr-Unit)
+```
+
 ## Discrete types are Segal types
 
 Discrete types are automatically Segal types.

src/simplicial-hott/10-rezk-types.rzk.md

@@ -692,54 +692,61 @@ The predicate `#!rzk is-iso-arrow` is a proposition.
 
 ## Rezk types
 
-A Segal type $A$ is a Rezk type just when, for all `#!rzk x y : A`, the natural
-map from `#!rzk x = y` to `#!rzk Iso A is-segal-A x y` is an equivalence.
+For every `x : A`, the identity arrow `id-hom A x : hom A x x` is an
+isomorphism.
 
 ```rzk
+#def is-iso-arrow-id-hom
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( x : A)
+  : is-iso-arrow A is-segal-A x x (id-hom A x)
+  :=
+    ( ( id-hom A x , comp-id-is-segal A is-segal-A x x (id-hom A x))
+    , ( id-hom A x , comp-id-is-segal A is-segal-A x x (id-hom A x)))
+
 #def iso-id-arrow
-  (A : U)
-  (is-segal-A : is-segal A)
+  ( A : U)
+  ( is-segal-A : is-segal A)
   : (x : A) → Iso A is-segal-A x x
+  := \ x → ( id-hom A x , is-iso-arrow-id-hom A is-segal-A x)
+```
+
+More generally, every path induces an isomorphism.
+
+```rzk
+#def is-iso-arrow-hom-eq
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( x y : A)
+  : ( p : x = y)
+  → is-iso-arrow A is-segal-A x y (hom-eq A x y p)
   :=
-    \ x →
-    (
-    (id-hom A x) ,
-    (
-    (
-      (id-hom A x) ,
-      (id-comp-is-segal A is-segal-A x x (id-hom A x))
-    ) ,
-    (
-      (id-hom A x) ,
-      (id-comp-is-segal A is-segal-A x x (id-hom A x))
-    )
-      )
-  )
+    ind-path A x
+    ( \ y' p' → is-iso-arrow A is-segal-A x y' (hom-eq A x y' p'))
+    ( is-iso-arrow-id-hom A is-segal-A x)
+    ( y)
 
 #def iso-eq
   ( A : U)
   ( is-segal-A : is-segal A)
   ( x y : A)
   : (x = y) → Iso A is-segal-A x y
-  :=
-    \ p →
-    ind-path
-      ( A)
-      ( x)
-      ( \ y' p' → Iso A is-segal-A x y')
-      ( iso-id-arrow A is-segal-A x)
-      ( y)
-      ( p)
+  := \ p → (hom-eq A x y p , is-iso-arrow-hom-eq A is-segal-A x y p)
 ```
 
+A Segal type `A` is a Rezk type just when, for all `#!rzk x y : A`, this natural
+map from `#!rzk x = y` to `#!rzk Iso A is-segal-A x y` is an equivalence.
+
 ```rzk title="RS17, Definition 10.6"
 #def is-rezk
   ( A : U)
   : U
   :=
-    Σ ( is-segal-A : is-segal A) ,
-      (x : A) → (y : A) →
-        is-equiv (x = y) (Iso A is-segal-A x y) (iso-eq A is-segal-A x y)
+    Σ ( is-segal-A : is-segal A)
+    , ( (x : A)
+      → (y : A)
+      → is-equiv (x = y) (Iso A is-segal-A x y) (iso-eq A is-segal-A x y))
 ```
 
 The inverse to `#!rzk iso-eq` for a Rezk type.
@@ -836,3 +843,101 @@ arrows.
       ( y)
       ( e)
 ```
+
+## Isomorphisms in discrete types
+
+In a discrete type every arrow is an isomorphisms. This is a straightforward
+path induction since every identity arrow is an isomorphism. Note that with
+extension extensionality, `is-discrete A` implies `is-segal A` but we state the
+first statement in a way that works without it.
+
+```rzk
+#def has-iso-arrows-is-segal-is-discrete
+  ( A : U)
+  ( is-discrete-A : is-discrete A)
+  ( is-segal-A : is-segal A)
+  ( x y : A)
+  : ( f : hom A x y)
+  → ( is-iso-arrow A is-segal-A x y f)
+  :=
+    ind-has-section-equiv (x =_{A} y) (hom A x y)
+    ( hom-eq A x y , is-discrete-A x y)
+    ( \ f → is-iso-arrow A is-segal-A x y f)
+    ( ind-path A x
+      ( \ y' p → is-iso-arrow A is-segal-A x y' (hom-eq A x y' p))
+      ( is-iso-arrow-id-hom A is-segal-A x)
+      ( y))
+
+#def has-iso-arrows-is-discrete uses (extext)
+  ( A : U)
+  ( is-discrete-A : is-discrete A)
+  ( x y : A)
+  ( f : hom A x y)
+  : ( is-iso-arrow A (is-segal-is-discrete extext A is-discrete-A)
+      x y f)
+  :=
+    has-iso-arrows-is-segal-is-discrete A
+    is-discrete-A
+    ( is-segal-is-discrete extext A is-discrete-A)
+    ( x) (y) (f)
+
+#def is-equiv-hom-iso-is-discrete uses (extext)
+  ( A : U)
+  ( is-discrete-A : is-discrete A)
+  ( x y : A)
+  : is-equiv
+    ( Iso A (is-segal-is-discrete extext A is-discrete-A)
+      x y)
+    ( hom A x y)
+    ( \ (f , _) → f)
+  :=
+    is-equiv-projection-contractible-fibers
+    ( hom A x y) (is-iso-arrow A (is-segal-is-discrete extext A is-discrete-A) x y)
+    ( \ f →
+      is-contr-is-inhabited-is-prop
+      ( is-iso-arrow A (is-segal-is-discrete extext A is-discrete-A) x y f)
+      ( is-prop-is-iso-arrow A
+        ( is-segal-is-discrete extext A is-discrete-A)
+        ( x) (y) (f))
+      ( has-iso-arrows-is-discrete A is-discrete-A x y f))
+```
+
+### Discrete types are Rezk
+
+As a corollary we obtain that every discrete type is Rezk.
+
+```rzk
+#def is-rezk-is-discrete uses (extext)
+  ( A : U)
+  : is-discrete A → is-rezk A
+  :=
+  \ is-discrete-A →
+  ( is-segal-is-discrete extext A is-discrete-A
+  , ( \ x y →
+      is-equiv-right-factor
+      ( x = y)
+      ( Iso A (is-segal-is-discrete extext A is-discrete-A)
+        x y)
+      ( hom A x y)
+      ( iso-eq A (is-segal-is-discrete extext A is-discrete-A)
+        x y)
+      ( \ (f , _) → f)
+      ( is-equiv-hom-iso-is-discrete A is-discrete-A x y)
+      ( is-discrete-A x y)))
+```
+
+In particular, every contractible type is Rezk
+
+```rzk
+#def is-rezk-is-contr uses (extext)
+  ( A : U)
+  : is-contr A → is-rezk A
+  :=
+  \ is-contr-A →
+    ( is-rezk-is-discrete A
+      ( is-discrete-is-contr extext A is-contr-A))
+
+#def is-rezk-Unit uses (extext)
+  : is-rezk Unit
+  := is-rezk-is-contr Unit (is-contr-Unit)
+```