# Extensions of maps

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2023-02-07.

module orthogonal-factorization-systems.extensions-of-maps where

Imports
open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
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.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.monomorphisms
open import foundation.postcomposition-functions
open import foundation.precomposition-dependent-functions
open import foundation.propositions
open import foundation.sets
open import foundation.structure-identity-principle
open import foundation.transport-along-identifications
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.torsorial-type-families

open import orthogonal-factorization-systems.local-types


## Idea

An extension of a map f : (x : A) → P x along a map i : A → B is a map g : (y : B) → Q y such that Q restricts along i to P and g restricts along i to f.

  A
|  \
i    f
|      \
∨       ∨
B - g -> P


## Definition

### Extensions of dependent functions

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
where

is-extension :
{P : B → UU l3} →
((x : A) → P (i x)) → ((y : B) → P y) → UU (l1 ⊔ l3)
is-extension f g = f ~ (g ∘ i)

extension-dependent-type :
(P : B → UU l3) →
((x : A) → P (i x)) → UU (l1 ⊔ l2 ⊔ l3)
extension-dependent-type P f = Σ ((y : B) → P y) (is-extension f)

extension :
{X : UU l3} → (A → X) → UU (l1 ⊔ l2 ⊔ l3)
extension {X} = extension-dependent-type (λ _ → X)

total-extension-dependent-type : (P : B → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
total-extension-dependent-type P =
Σ ((x : A) → P (i x)) (extension-dependent-type P)

total-extension : (X : UU l3) → UU (l1 ⊔ l2 ⊔ l3)
total-extension X = total-extension-dependent-type (λ _ → X)

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {i : A → B}
{P : B → UU l3} {f : (x : A) → P (i x)}
where

map-extension : extension-dependent-type i P f → (y : B) → P y
map-extension = pr1

is-extension-map-extension :
(E : extension-dependent-type i P f) → is-extension i f (map-extension E)
is-extension-map-extension = pr2


## Operations

### Vertical composition of extensions of maps

  A
|  \
i    f
|      \
∨       ∨
B - g -> P
|       ∧
j      /
|    h
∨  /
C

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4}
{i : A → B} {j : B → C}
{f : (x : A) → P (j (i x))} {g : (x : B) → P (j x)} {h : (x : C) → P x}
where

is-extension-comp-vertical :
is-extension j g h → is-extension i f g → is-extension (j ∘ i) f h
is-extension-comp-vertical H G x = G x ∙ H (i x)


### Horizontal composition of extensions of maps

           A
/  |  \
f    g    h
/      |      \
∨       ∨       ∨
B - i -> C - j -> P


#### Horizontal composition of extensions of dependent functions

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4}
{f : A → B} {g : A → C} {h : (x : A) → P (g x)}
{i : B → C} {j : (z : C) → P z}
where

is-extension-dependent-type-comp-horizontal :
(I : is-extension f g i) →
is-extension g h j → is-extension f (λ x → tr P (I x) (h x)) (j ∘ i)
is-extension-dependent-type-comp-horizontal I J x =
ap (tr P (I x)) (J x) ∙ apd j (I x)


#### Horizontal composition of extensions of ordinary maps

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
{f : A → B} {g : A → C} {h : A → X}
{i : B → C} {j : C → X}
where

is-extension-comp-horizontal :
(I : is-extension f g i) → is-extension g h j → is-extension f h (j ∘ i)
is-extension-comp-horizontal I J x = (J x) ∙ ap j (I x)


### Left whiskering of extensions of maps

  A
|  \
i    f
|      \
∨       ∨
B - g -> C - h -> P

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {P : C → UU l4}
{i : A → B} {f : A → C} {g : B → C}
where

is-extension-left-whisker :
(h : (x : C) → P x) (F : is-extension i f g) →
(is-extension i (λ x → tr P (F x) (h (f x))) (h ∘ g))
is-extension-left-whisker h F = apd h ∘ F


### Right whiskering of extensions of maps

  X - h -> A
|  \
i    f
|      \
∨       ∨
B - g -> P

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {P : B → UU l3} {X : UU l4}
{i : A → B} {f : (x : A) → P (i x)} {g : (y : B) → P y}
where

is-extension-right-whisker :
(F : is-extension i f g) (h : X → A) → is-extension (i ∘ h) (f ∘ h) g
is-extension-right-whisker F h = F ∘ h


### Postcomposition of extensions

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
where

postcomp-extension :
(f : A → B) (i : A → X) (g : X → Y) →
extension f i → extension f (g ∘ i)
postcomp-extension f i g =
map-Σ (is-extension f (g ∘ i)) (postcomp B g) (λ j H → g ·l H)


## Properties

### Characterizing identifications of extensions of maps

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
{P : B → UU l3}
(f : (x : A) → P (i x))
where

coherence-htpy-extension :
(e e' : extension-dependent-type i P f) →
map-extension e ~ map-extension e' → UU (l1 ⊔ l3)
coherence-htpy-extension e e' K =
(is-extension-map-extension e ∙h (K ·r i)) ~ is-extension-map-extension e'

htpy-extension : (e e' : extension-dependent-type i P f) → UU (l1 ⊔ l2 ⊔ l3)
htpy-extension e e' =
Σ ( map-extension e ~ map-extension e')
( coherence-htpy-extension e e')

refl-htpy-extension :
(e : extension-dependent-type i P f) → htpy-extension e e
pr1 (refl-htpy-extension e) = refl-htpy
pr2 (refl-htpy-extension e) = right-unit-htpy

htpy-eq-extension :
(e e' : extension-dependent-type i P f) → e ＝ e' → htpy-extension e e'
htpy-eq-extension e .e refl = refl-htpy-extension e

is-torsorial-htpy-extension :
(e : extension-dependent-type i P f) → is-torsorial (htpy-extension e)
is-torsorial-htpy-extension e =
is-torsorial-Eq-structure
( is-torsorial-htpy (map-extension e))
( map-extension e , refl-htpy)
( is-torsorial-htpy (is-extension-map-extension e ∙h refl-htpy))

is-equiv-htpy-eq-extension :
(e e' : extension-dependent-type i P f) → is-equiv (htpy-eq-extension e e')
is-equiv-htpy-eq-extension e =
fundamental-theorem-id
( is-torsorial-htpy-extension e)
( htpy-eq-extension e)

extensionality-extension :
(e e' : extension-dependent-type i P f) → (e ＝ e') ≃ (htpy-extension e e')
pr1 (extensionality-extension e e') = htpy-eq-extension e e'
pr2 (extensionality-extension e e') = is-equiv-htpy-eq-extension e e'

eq-htpy-extension :
(e e' : extension-dependent-type i P f)
(H : map-extension e ~ map-extension e') →
coherence-htpy-extension e e' H → e ＝ e'
eq-htpy-extension e e' H K =
map-inv-equiv (extensionality-extension e e') (H , K)


### The total type of extensions is equivalent to (y : B) → P y

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
where

inv-compute-total-extension-dependent-type :
{P : B → UU l3} → total-extension-dependent-type i P ≃ ((y : B) → P y)
inv-compute-total-extension-dependent-type =
( right-unit-law-Σ-is-contr (λ f → is-torsorial-htpy' (f ∘ i))) ∘e
( equiv-left-swap-Σ)

compute-total-extension-dependent-type :
{P : B → UU l3} → ((y : B) → P y) ≃ total-extension-dependent-type i P
compute-total-extension-dependent-type =
inv-equiv (inv-compute-total-extension-dependent-type)

inv-compute-total-extension :
{X : UU l3} → total-extension i X ≃ (B → X)
inv-compute-total-extension = inv-compute-total-extension-dependent-type

compute-total-extension :
{X : UU l3} → (B → X) ≃ total-extension i X
compute-total-extension = compute-total-extension-dependent-type


### The truncation level of the type of extensions is bounded by the truncation level of the codomains

module _
{l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (i : A → B)
where

is-trunc-is-extension-dependent-type :
{P : B → UU l3} (f : (x : A) → P (i x)) →
((x : A) → is-trunc (succ-𝕋 k) (P (i x))) →
(g : (x : B) → P x) → is-trunc k (is-extension i f g)
is-trunc-is-extension-dependent-type f is-trunc-P g =
is-trunc-Π k λ x → is-trunc-P x (f x) (g (i x))

is-trunc-extension-dependent-type :
{P : B → UU l3} (f : (x : A) → P (i x)) →
((x : B) → is-trunc k (P x)) → is-trunc k (extension-dependent-type i P f)
is-trunc-extension-dependent-type f is-trunc-P =
is-trunc-Σ
( is-trunc-Π k is-trunc-P)
( is-trunc-is-extension-dependent-type f
( is-trunc-succ-is-trunc k ∘ (is-trunc-P ∘ i)))

is-trunc-total-extension-dependent-type :
{P : B → UU l3} →
((x : B) → is-trunc k (P x)) →
is-trunc k (total-extension-dependent-type i P)
is-trunc-total-extension-dependent-type {P} is-trunc-P =
is-trunc-equiv' k
( (y : B) → P y)
( compute-total-extension-dependent-type i)
( is-trunc-Π k is-trunc-P)

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A → B)
where

is-contr-is-extension :
{P : B → UU l3} (f : (x : A) → P (i x)) →
((x : A) → is-prop (P (i x))) →
(g : (x : B) → P x) → is-contr (is-extension i f g)
is-contr-is-extension f is-prop-P g =
is-contr-Π λ x → is-prop-P x (f x) (g (i x))

is-prop-is-extension :
{P : B → UU l3} (f : (x : A) → P (i x)) →
((x : A) → is-set (P (i x))) →
(g : (x : B) → P x) → is-prop (is-extension i f g)
is-prop-is-extension f is-set-P g =
is-prop-Π (λ x → is-set-P x (f x) (g (i x)))


### Every map has a unique extension along i if and only if P is i-local

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (i : A → B)
{l : Level} (P : B → UU l)
where

equiv-fiber'-precomp-extension-dependent-type :
(f : (x : A) → P (i x)) →
fiber' (precomp-Π i P) f ≃ extension-dependent-type i P f
equiv-fiber'-precomp-extension-dependent-type f =
equiv-tot (λ g → equiv-funext {f = f} {g ∘ i})

equiv-fiber-precomp-extension-dependent-type :
(f : (x : A) → P (i x)) →
fiber (precomp-Π i P) f ≃ extension-dependent-type i P f
equiv-fiber-precomp-extension-dependent-type f =
( equiv-fiber'-precomp-extension-dependent-type f) ∘e
( equiv-fiber (precomp-Π i P) f)

equiv-is-contr-extension-dependent-type-is-local-dependent-type :
is-local-dependent-type i P ≃
((f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f))
equiv-is-contr-extension-dependent-type-is-local-dependent-type =
( equiv-Π-equiv-family
( equiv-is-contr-equiv ∘ equiv-fiber-precomp-extension-dependent-type)) ∘e
( equiv-is-contr-map-is-equiv (precomp-Π i P))

is-contr-extension-dependent-type-is-local-dependent-type :
is-local-dependent-type i P →
(f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f)
is-contr-extension-dependent-type-is-local-dependent-type =
map-equiv equiv-is-contr-extension-dependent-type-is-local-dependent-type

is-local-dependent-type-is-contr-extension-dependent-type :
((f : (x : A) → P (i x)) → is-contr (extension-dependent-type i P f)) →
is-local-dependent-type i P
is-local-dependent-type-is-contr-extension-dependent-type =
map-inv-equiv
equiv-is-contr-extension-dependent-type-is-local-dependent-type


## Examples

### Every map is an extension of itself along the identity

is-extension-self :
{l1 l2 : Level} {A : UU l1} {P : A → UU l2}
(f : (x : A) → P x) → is-extension id f f
is-extension-self _ = refl-htpy


### The identity is an extension of every map along themselves

is-extension-along-self :
{l1 l2 : Level} {A : UU l1} {B : UU l2}
(f : A → B) → is-extension f f id
is-extension-along-self _ = refl-htpy


### Postcomposition of extensions by an embedding is an embedding

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
where

is-emb-postcomp-extension :
(f : A → B) (i : A → X) (g : X → Y) → is-emb g →
is-emb (postcomp-extension f i g)
is-emb-postcomp-extension f i g H =
is-emb-map-Σ
( is-extension f (g ∘ i))
( is-mono-is-emb g H B)
( λ j →
is-emb-is-equiv
( is-equiv-map-Π-is-fiberwise-equiv
( λ x → H (i x) (j (f x)))))