# The pullback-hom

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

Created on 2023-02-18.

module orthogonal-factorization-systems.pullback-hom where

Imports
open import foundation.action-on-identifications-functions
open import foundation.cones-over-cospans
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibered-maps
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.morphisms-cospans
open import foundation.pullbacks
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universal-property-pullbacks
open import foundation.universe-levels
open import foundation.whiskering-homotopies

open import orthogonal-factorization-systems.lifting-squares


## Idea

Given a pair of maps f : A → B and g : X → Y, there is a commuting square

          - ∘ f
B → X ----> A → X
|           |
g ∘ - |           | g ∘ -
V           V
B → Y ----> A → Y.
- ∘ f


The pullback-hom of f and g, f ⋔ g, is the comparison map from B → X to the pullback of the cospan:

      ∙ ------> A → X
|  ⌟        |
|           | g ∘ -
V           V
B → Y ----> A → Y.
- ∘ f


This pullback type can be understood as the type of fibered maps from f to g, i.e. commuting squares where the vertical maps are f and g.

## Definitions

### The codomain of the pullback-hom

type-canonical-pullback-hom :
{l1 l2 l3 l4 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) →
UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
type-canonical-pullback-hom {A = A} {Y = Y} f g =
canonical-pullback (precomp f Y) (postcomp A g)


#### The canonical pullback-hom type is equivalent to the type of fibered maps

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

equiv-fibered-map-type-canonical-pullback-hom :
type-canonical-pullback-hom f g ≃ fibered-map f g
equiv-fibered-map-type-canonical-pullback-hom =
equiv-tot (λ _ → equiv-tot (λ _ → equiv-funext))

equiv-type-canonical-pullback-hom-fibered-map :
fibered-map f g ≃ type-canonical-pullback-hom f g
equiv-type-canonical-pullback-hom-fibered-map =
inv-equiv equiv-fibered-map-type-canonical-pullback-hom

map-fibered-map-type-canonical-pullback-hom :
type-canonical-pullback-hom f g → fibered-map f g
map-fibered-map-type-canonical-pullback-hom =
map-equiv equiv-fibered-map-type-canonical-pullback-hom

map-type-canonical-pullback-hom-fibered-map :
fibered-map f g → type-canonical-pullback-hom f g
map-type-canonical-pullback-hom-fibered-map =
map-equiv equiv-type-canonical-pullback-hom-fibered-map


Below are basic definitions related to the pullback property of the type of fibered maps.

  cone-canonical-pullback-hom :
cone (precomp f Y) (postcomp A g) (type-canonical-pullback-hom f g)
cone-canonical-pullback-hom =
cone-canonical-pullback (precomp f Y) (postcomp A g)

cone-pullback-hom :
cone (precomp f Y) (postcomp A g) (fibered-map f g)
cone-pullback-hom =
cone-map
( precomp f Y)
( postcomp A g)
( cone-canonical-pullback (precomp f Y) (postcomp A g))
( map-type-canonical-pullback-hom-fibered-map)

gap-canonical-pullback-hom :
{l : Level} {C : UU l} →
cone (precomp f Y) (postcomp A g) C → C → type-canonical-pullback-hom f g
gap-canonical-pullback-hom = gap (precomp f Y) (postcomp A g)

gap-pullback-hom :
{l : Level} {C : UU l} →
cone (precomp f Y) (postcomp A g) C → C → fibered-map f g
gap-pullback-hom c x =
map-fibered-map-type-canonical-pullback-hom (gap-canonical-pullback-hom c x)

is-pullback-fibered-map :
is-pullback (precomp f Y) (postcomp A g) (cone-pullback-hom)
is-pullback-fibered-map =
is-equiv-map-equiv equiv-type-canonical-pullback-hom-fibered-map

universal-property-pullback-fibered-map :
{l : Level} →
universal-property-pullback l
( precomp f Y) (postcomp A g) (cone-pullback-hom)
universal-property-pullback-fibered-map =
universal-property-pullback-is-pullback
( precomp f Y)
( postcomp A g)
( cone-pullback-hom)
( is-pullback-fibered-map)


### The pullback-hom map

The pullback-hom f ⋔ g is the map (B → X) → fibered-map f g, that takes a diagonal map j from the codomain of f to the domain of g to the fibered map (g ∘ j , j ∘ f , refl-htpy).

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

pullback-hom : (B → X) → fibered-map f g
pullback-hom = gap-pullback-hom f g (postcomp B g , precomp f X , refl-htpy)

infix 30 _⋔_
_⋔_ = pullback-hom


The symbol ⋔ is the pitchfork (agda-input: \pitchfork).

## Properties

### Functoriality of the pullback-hom

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y)
{l1' l2' l3' l4' : Level}
{A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {Y' : UU l4'}
(f' : A' → B') (g' : X' → Y')
where

map-pullback-hom :
hom-cospan
( precomp f' Y')
( postcomp A' g')
( precomp f Y)
( postcomp A g) →
fibered-map f' g' → fibered-map f g
map-pullback-hom =
map-is-pullback
( precomp f Y)
( postcomp A g)
( precomp f' Y')
( postcomp A' g')
( cone-pullback-hom f g)
( cone-pullback-hom f' g')
( is-pullback-fibered-map f g)
( is-pullback-fibered-map f' g')


### The fibers of the pullback-hom

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (h : fibered-map f g)
where

inv-compute-fiber-pullback-hom :
(fiber (pullback-hom f g) h) ≃ (lifting-square-fibered-map f g h)
inv-compute-fiber-pullback-hom =
equiv-tot
( λ j →
( equiv-Σ _
( equiv-inv-htpy (j ∘ f) (map-total-fibered-map f g h))
( λ E →
equiv-Σ _
( equiv-inv-htpy (g ∘ j) (map-base-fibered-map f g h))
( λ L →
( equiv-concat-htpy'
( inv-htpy L ·r f)
( λ x →
ap
( is-map-over-map-total-fibered-map f g h x ∙_)
( inv-htpy-left-whisk-inv-htpy g E x))) ∘e
( ( equiv-right-transpose-htpy-concat
( inv-htpy (L ·r f))
( g ·l E)
( is-map-over-map-total-fibered-map f g h)) ∘e
( equiv-left-transpose-htpy-concat'
( g ·l E)
( L ·r f)
( is-map-over-map-total-fibered-map f g h)))))) ∘e
( ( equiv-left-swap-Σ) ∘e
( extensionality-fibered-map f g (pullback-hom f g j) h)))

compute-fiber-pullback-hom :
(lifting-square-fibered-map f g h) ≃ (fiber (pullback-hom f g) h)
compute-fiber-pullback-hom = inv-equiv inv-compute-fiber-pullback-hom