Null maps, null types and null type families (#1088)

Defines `Y`-null maps, `Y`-null types and `Y`-null type families, and
establishes a few basic properties of these. Also formalizes the fiber
condition for orthogonal maps. Part of #930. Depends on #1086.

- If `A` is a retract of `B` and `S` is a retract of `T` then
`diagonal-exponential A S` is a retract of `diagonal-exponential B T`.
- Null types
  - Null types are closed under equivalences in the base and exponent
  - Null types are closed under retracts in the base and exponent
- A type is `Y`-null if and only if the terminal projection of `Y` is
orthogonal to the terminal projection of `A`
- Null families
- Null families are closed under equivalences in the family and exponent
  - Null families are closed under retracts in the family and exponent
- Null maps, equivalence of
  - Fiber condition
  - Pullback condition
  - Right orthogonal map to terminal projection condition
  - Local at terminal projection condition
- Fiber condition for orthogonal maps

src/foundation-core/retracts-of-types.lagda.md

@@ -14,6 +14,7 @@ open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.function-types
+open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.postcomposition-functions
 open import foundation-core.precomposition-functions
@@ -168,6 +169,17 @@ module _
     eq-htpy (is-retraction-map-retraction-retract R ·r h)
 ```
 
+### Every type is a retract of itself
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  id-retract : A retract-of A
+  id-retract = (id , id , refl-htpy)
+```
+
 ### Composition of retracts
 
 ```agda

src/foundation/constant-maps.lagda.md

@@ -15,11 +15,20 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.faithful-maps
 open import foundation.function-extensionality
+open import foundation.functoriality-dependent-pair-types
+open import foundation.morphisms-arrows
+open import foundation.postcomposition-functions
+open import foundation.retracts-of-maps
+open import foundation.retracts-of-types
+open import foundation.transposition-identifications-along-equivalences
 open import foundation.type-arithmetic-unit-type
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
 open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.1-types
+open import foundation-core.commuting-squares-of-maps
 open import foundation-core.contractible-maps
 open import foundation-core.embeddings
 open import foundation-core.equivalences
@@ -55,16 +64,21 @@ module _
   compute-action-htpy-function-const c H = ap-const c (eq-htpy H)
 ```
 
+### Computing the fibers of point inclusions
+
+```agda
+compute-fiber-point :
+  {l : Level} {A : UU l} (x y : A) → fiber (point x) y ≃ (x ＝ y)
+compute-fiber-point x y = left-unit-law-product
+```
+
 ### A type is `k+1`-truncated if and only if all point inclusions are `k`-truncated maps
 
 ```agda
 module _
   {l : Level} {A : UU l}
   where
 
-  compute-fiber-point : (x y : A) → fiber (point x) y ≃ (x ＝ y)
-  compute-fiber-point x y = left-unit-law-product
-
   abstract
     is-trunc-map-point-is-trunc :
       (k : 𝕋) → is-trunc (succ-𝕋 k) A →

src/foundation/diagonal-maps-of-types.lagda.md

@@ -11,6 +11,11 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.function-extensionality
+open import foundation.functoriality-dependent-pair-types
+open import foundation.morphisms-arrows
+open import foundation.postcomposition-functions
+open import foundation.retracts-of-types
+open import foundation.transposition-identifications-along-equivalences
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
@@ -80,3 +85,36 @@ module _
   pr1 diagonal-exponential-injection = diagonal-exponential A B
   pr2 diagonal-exponential-injection = is-injective-diagonal-exponential
 ```
+
+### The action on identifications of an (exponential) diagonal is a diagonal
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1) {B : UU l2} (x y : B)
+  where
+
+  compute-htpy-eq-ap-diagonal-exponential :
+    htpy-eq ∘ ap (diagonal-exponential B A) ~ diagonal-exponential (x ＝ y) A
+  compute-htpy-eq-ap-diagonal-exponential refl = refl
+
+  inv-compute-htpy-eq-ap-diagonal-exponential :
+    diagonal-exponential (x ＝ y) A ~ htpy-eq ∘ ap (diagonal-exponential B A)
+  inv-compute-htpy-eq-ap-diagonal-exponential =
+    inv-htpy compute-htpy-eq-ap-diagonal-exponential
+
+  compute-eq-htpy-ap-diagonal-exponential :
+    ap (diagonal-exponential B A) ~ eq-htpy ∘ diagonal-exponential (x ＝ y) A
+  compute-eq-htpy-ap-diagonal-exponential p =
+    map-eq-transpose-equiv
+      ( equiv-funext)
+      ( compute-htpy-eq-ap-diagonal-exponential p)
+```
+
+### Computing the fibers of diagonal maps
+
+```agda
+compute-fiber-diagonal-exponential :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
+  fiber (diagonal-exponential B A) f ≃ Σ B (λ b → (x : A) → b ＝ f x)
+compute-fiber-diagonal-exponential f = equiv-tot (λ _ → equiv-funext)
+```

src/foundation/retracts-of-maps.lagda.md

@@ -11,16 +11,19 @@ open import foundation.action-on-identifications-functions
 open import foundation.commuting-prisms-of-maps
 open import foundation.commuting-triangles-of-morphisms-arrows
 open import foundation.dependent-pair-types
+open import foundation.diagonal-maps-of-types
 open import foundation.function-extensionality
 open import foundation.functoriality-fibers-of-maps
 open import foundation.homotopies-morphisms-arrows
+open import foundation.homotopy-algebra
 open import foundation.morphisms-arrows
 open import foundation.postcomposition-functions
 open import foundation.precomposition-functions
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.commuting-squares-of-maps
+open import foundation-core.constant-maps
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
@@ -904,6 +907,75 @@ module _
   pr2 retract-map-postcomp-retract-map = retraction-postcomp-retract-map
 ```
 
+### If `A` is a retract of `B` and `S` is a retract of `T` then `diagonal-exponential A S` is a retract of `diagonal-exponential B T`
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {S : UU l3} {T : UU l4}
+  (R : A retract-of B) (Q : S retract-of T)
+  where
+
+  inclusion-diagonal-exponential-retract :
+    hom-arrow (diagonal-exponential A S) (diagonal-exponential B T)
+  inclusion-diagonal-exponential-retract =
+    ( inclusion-retract R ,
+      precomp (map-retraction-retract Q) B ∘ postcomp S (inclusion-retract R) ,
+      refl-htpy)
+
+  hom-retraction-diagonal-exponential-retract :
+    hom-arrow (diagonal-exponential B T) (diagonal-exponential A S)
+  hom-retraction-diagonal-exponential-retract =
+    ( map-retraction-retract R ,
+      postcomp S (map-retraction-retract R) ∘ precomp (inclusion-retract Q) B ,
+      refl-htpy)
+
+  coh-retract-map-diagonal-exponential-retract :
+    coherence-retract-map
+      ( diagonal-exponential A S)
+      ( diagonal-exponential B T)
+      ( inclusion-diagonal-exponential-retract)
+      ( hom-retraction-diagonal-exponential-retract)
+      ( is-retraction-map-retraction-retract R)
+      ( horizontal-concat-htpy
+        ( htpy-postcomp S (is-retraction-map-retraction-retract R))
+        ( htpy-precomp (is-retraction-map-retraction-retract Q) A))
+  coh-retract-map-diagonal-exponential-retract x =
+    ( compute-eq-htpy-ap-diagonal-exponential S
+      ( map-retraction-retract R (inclusion-retract R x))
+      ( x)
+      ( is-retraction-map-retraction-retract R x)) ∙
+    ( ap
+      ( λ p →
+        ( ap (λ f a → map-retraction-retract R (inclusion-retract R (f a))) p) ∙
+        ( eq-htpy (λ _ → is-retraction-map-retraction-retract R x)))
+      ( inv
+        ( ( ap
+            ( eq-htpy)
+            ( eq-htpy (ap-const x ·r is-retraction-map-retraction-retract Q))) ∙
+          ( eq-htpy-refl-htpy (diagonal-exponential A S x))))) ∙
+      ( inv right-unit)
+
+  is-retraction-hom-retraction-diagonal-exponential-retract :
+    is-retraction-hom-arrow
+      ( diagonal-exponential A S)
+      ( diagonal-exponential B T)
+      ( inclusion-diagonal-exponential-retract)
+      ( hom-retraction-diagonal-exponential-retract)
+  is-retraction-hom-retraction-diagonal-exponential-retract =
+    ( ( is-retraction-map-retraction-retract R) ,
+      ( horizontal-concat-htpy
+        ( htpy-postcomp S (is-retraction-map-retraction-retract R))
+        ( htpy-precomp (is-retraction-map-retraction-retract Q) A)) ,
+      ( coh-retract-map-diagonal-exponential-retract))
+
+  retract-map-diagonal-exponential-retract :
+    (diagonal-exponential A S) retract-of-map (diagonal-exponential B T)
+  retract-map-diagonal-exponential-retract =
+    ( inclusion-diagonal-exponential-retract ,
+      hom-retraction-diagonal-exponential-retract ,
+      is-retraction-hom-retraction-diagonal-exponential-retract)
+```
+
 ## References
 
 {{#bibliography}} {{#reference UF13}}

src/orthogonal-factorization-systems.lagda.md

@@ -42,6 +42,8 @@ open import orthogonal-factorization-systems.mere-lifting-properties public
 open import orthogonal-factorization-systems.modal-induction public
 open import orthogonal-factorization-systems.modal-operators public
 open import orthogonal-factorization-systems.modal-subuniverse-induction public
+open import orthogonal-factorization-systems.null-families-of-types public
+open import orthogonal-factorization-systems.null-maps public
 open import orthogonal-factorization-systems.null-types public
 open import orthogonal-factorization-systems.open-modalities public
 open import orthogonal-factorization-systems.orthogonal-factorization-systems public

src/orthogonal-factorization-systems/local-families-of-types.lagda.md

@@ -23,15 +23,15 @@ open import orthogonal-factorization-systems.orthogonal-maps
 
 A family of types `B : A → UU l` is said to be
 {{#concept "local" Disambiguation="family of types" Agda=is-local-family}} at
-`f : Y → X`, or **`f`-local**, if every
+`f : X → Y`, or **`f`-local**, if every
 [fiber](foundation-core.fibers-of-maps.md) is.
 
 ## Definition
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {Y : UU l1} {X : UU l2}
-  (f : Y → X) {A : UU l3} (B : A → UU l4)
+  {l1 l2 l3 l4 : Level} {X : UU l1} {Y : UU l2}
+  (f : X → Y) {A : UU l3} (B : A → UU l4)
   where
 
   is-local-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)

src/orthogonal-factorization-systems/local-maps.lagda.md

@@ -7,34 +7,54 @@ module orthogonal-factorization-systems.local-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.cartesian-morphisms-arrows
+open import foundation.cones-over-cospan-diagrams
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.equivalences-arrows
 open import foundation.fibers-of-maps
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-fibers-of-maps
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.postcomposition-functions
+open import foundation.precomposition-functions
 open import foundation.propositions
+open import foundation.pullbacks
 open import foundation.unit-type
+open import foundation.universal-property-family-of-fibers-of-maps
 open import foundation.universe-levels
 
 open import orthogonal-factorization-systems.local-families-of-types
 open import orthogonal-factorization-systems.local-types
 open import orthogonal-factorization-systems.orthogonal-maps
+open import orthogonal-factorization-systems.pullback-hom
 ```
 
 </details>
 
 ## Idea
 
-A map `g : A → B` is said to be
+A map `g : X → Y` is said to be
 {{#concept "local" Disambiguation="maps of types" Agda=is-local-map}} at
-`f : Y → X`, or
+`f : A → B`, or
 {{#concept "`f`-local" Disambiguation="maps of types" Agda=is-local-map}}, if
 all its [fibers](foundation-core.fibers-of-maps.md) are
 [`f`-local types](orthogonal-factorization-systems.local-types.md).
 
+Equivalently, the map `g` is `f`-local if and only if `f` is
+[orthogonal](orthogonal-factorization-systems.orthogonal-maps.md) to `g`.
+
 ## Definition
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {Y : UU l1} {X : UU l2} {A : UU l3} {B : UU l4}
-  (f : Y → X) (g : A → B)
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y)
   where
 
   is-local-map : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
@@ -51,17 +71,17 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {Y : UU l1} {X : UU l2} {B : UU l3}
-  (f : Y → X)
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {Y : UU l3}
+  (f : A → B)
   where
 
   is-local-is-local-terminal-map :
-    is-local-map f (terminal-map B) → is-local f B
+    is-local-map f (terminal-map Y) → is-local f Y
   is-local-is-local-terminal-map H =
     is-local-equiv f (inv-equiv-fiber-terminal-map star) (H star)
 
   is-local-terminal-map-is-local :
-    is-local f B → is-local-map f (terminal-map B)
+    is-local f Y → is-local-map f (terminal-map Y)
   is-local-terminal-map-is-local H u =
     is-local-equiv f (equiv-fiber-terminal-map u) H
 ```
@@ -70,8 +90,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 l6 : Level}
-  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {X' : UU l5} {Y' : UU l6}
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
   (f : A → B) (g : X → Y)
   where