# Cartesian morphisms of arrows

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-01-25.

module foundation.cartesian-morphisms-arrows where

Imports
open import foundation.action-on-identifications-functions
open import foundation.commuting-triangles-of-maps
open import foundation.commuting-triangles-of-morphisms-arrows
open import foundation.cones-over-cospan-diagrams
open import foundation.coproducts-pullbacks
open import foundation.dependent-pair-types
open import foundation.dependent-products-pullbacks
open import foundation.dependent-sums-pullbacks
open import foundation.diagonal-maps-cartesian-products-of-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies-morphisms-arrows
open import foundation.identity-types
open import foundation.morphisms-arrows
open import foundation.postcomposition-functions
open import foundation.postcomposition-pullbacks
open import foundation.products-pullbacks
open import foundation.pullbacks
open import foundation.standard-pullbacks
open import foundation.unit-type
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-maps
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.universal-property-pullbacks


## Idea

A morphism of arrows h : f → g is said to be cartesian if the commuting square

        i
A -----> X
|        |
f |   h    | g
∨        ∨
B -----> Y
j


is a pullback square. In this instance, we also say that f is a base change of g.

## Definitions

### The predicate of being a cartesian morphism of arrows

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 : hom-arrow f g)
where

is-cartesian-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
is-cartesian-hom-arrow =
is-pullback (map-codomain-hom-arrow f g h) g (cone-hom-arrow f g h)

is-prop-is-cartesian-hom-arrow : is-prop is-cartesian-hom-arrow
is-prop-is-cartesian-hom-arrow =
is-prop-is-pullback (map-codomain-hom-arrow f g h) g (cone-hom-arrow f g h)

is-cartesian-hom-arrow-Prop : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
pr1 is-cartesian-hom-arrow-Prop = is-cartesian-hom-arrow
pr2 is-cartesian-hom-arrow-Prop = is-prop-is-cartesian-hom-arrow


### The type of cartesian morphisms of arrows

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

cartesian-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
cartesian-hom-arrow = Σ (hom-arrow f g) (is-cartesian-hom-arrow f g)

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 : cartesian-hom-arrow f g)
where

hom-arrow-cartesian-hom-arrow : hom-arrow f g
hom-arrow-cartesian-hom-arrow = pr1 h

is-cartesian-cartesian-hom-arrow :
is-cartesian-hom-arrow f g hom-arrow-cartesian-hom-arrow
is-cartesian-cartesian-hom-arrow = pr2 h

map-domain-cartesian-hom-arrow : A → X
map-domain-cartesian-hom-arrow =
map-domain-hom-arrow f g hom-arrow-cartesian-hom-arrow

map-codomain-cartesian-hom-arrow : B → Y
map-codomain-cartesian-hom-arrow =
map-codomain-hom-arrow f g hom-arrow-cartesian-hom-arrow

coh-cartesian-hom-arrow :
coherence-square-maps
( map-domain-cartesian-hom-arrow)
( f)
( g)
( map-codomain-cartesian-hom-arrow)
coh-cartesian-hom-arrow =
coh-hom-arrow f g hom-arrow-cartesian-hom-arrow

cone-cartesian-hom-arrow :
cone map-codomain-cartesian-hom-arrow g A
cone-cartesian-hom-arrow =
cone-hom-arrow f g hom-arrow-cartesian-hom-arrow

universal-property-cartesian-hom-arrow :
universal-property-pullback
( map-codomain-cartesian-hom-arrow)
( g)
( cone-cartesian-hom-arrow)
universal-property-cartesian-hom-arrow =
universal-property-pullback-is-pullback
( map-codomain-cartesian-hom-arrow)
( g)
( cone-cartesian-hom-arrow)
( is-cartesian-cartesian-hom-arrow)


## Properties

### Cartesian morphisms of arrows arising from standard pullbacks

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

standard-pullback-cartesian-hom-arrow :
cartesian-hom-arrow vertical-map-standard-pullback g
standard-pullback-cartesian-hom-arrow =
( hom-arrow-cone f g (cone-standard-pullback f g) , is-equiv-id)


### Cartesian morphisms of arrows arising from fibers

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (y : B)
where

fiber-cartesian-hom-arrow :
cartesian-hom-arrow (terminal-map (fiber f y)) f
pr1 fiber-cartesian-hom-arrow =
hom-arrow-cone (point y) f (swap-cone f (point y) (cone-fiber f y))
pr2 fiber-cartesian-hom-arrow =
is-pullback-swap-cone f (point y)
( cone-fiber f y)
( is-pullback-cone-fiber f y)


### Transposing cartesian morphisms of arrows

The transposition of a cartesian morphism of arrows

        i
A -----> X
| ⌟      |
f |        | g
∨        ∨
B -----> Y
j


is the cartesian morphism of arrows

        f
A -----> B
| ⌟      |
i |        | j
∨        ∨
X -----> Y.
g

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

is-cartesian-transpose-cartesian-hom-arrow :
is-cartesian-hom-arrow
( map-domain-cartesian-hom-arrow f g α)
( map-codomain-cartesian-hom-arrow f g α)
( transpose-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α))
is-cartesian-transpose-cartesian-hom-arrow =
is-pullback-swap-cone
( map-codomain-cartesian-hom-arrow f g α)
( g)
( cone-cartesian-hom-arrow f g α)
( is-cartesian-cartesian-hom-arrow f g α)

transpose-cartesian-hom-arrow :
cartesian-hom-arrow
( map-domain-cartesian-hom-arrow f g α)
( map-codomain-cartesian-hom-arrow f g α)
transpose-cartesian-hom-arrow =
( transpose-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α) ,
is-cartesian-transpose-cartesian-hom-arrow)


### If the target of a cartesian morphism is an equivalence then so is the source

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

is-equiv-source-is-equiv-target-cartesian-hom-arrow : is-equiv g → is-equiv f
is-equiv-source-is-equiv-target-cartesian-hom-arrow G =
is-equiv-vertical-map-is-pullback
( map-codomain-cartesian-hom-arrow f g α)
( g)
( cone-cartesian-hom-arrow f g α)
( G)
( is-cartesian-cartesian-hom-arrow f g α)


### If the target and source of a morphism of arrows are equivalences then the morphism is cartesian

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

is-cartesian-hom-arrow-is-equiv-source-is-equiv-target :
is-equiv g → is-equiv f → is-cartesian-hom-arrow f g α
is-cartesian-hom-arrow-is-equiv-source-is-equiv-target =
is-pullback-is-equiv-vertical-maps
( map-codomain-hom-arrow f g α)
( g)
( cone-hom-arrow f g α)


### Cartesian morphisms of arrows are preserved under homotopies of arrows

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

abstract
is-cartesian-hom-arrow-htpy :
{f f' : A → B} (F' : f' ~ f) {g g' : X → Y} (G : g ~ g')
(α : hom-arrow f g) →
is-cartesian-hom-arrow f g α →
is-cartesian-hom-arrow f' g' (hom-arrow-htpy F' G α)
is-cartesian-hom-arrow-htpy {f} F' {g} G α =
is-pullback-htpy
( refl-htpy)
( inv-htpy G)
( cone-hom-arrow f g α)
( ( F') ,
( refl-htpy) ,
( ( assoc-htpy
( map-codomain-hom-arrow f g α ·l F' ∙h coh-hom-arrow f g α)
( G ·r map-domain-hom-arrow f g α)
( inv-htpy (G ·r map-domain-hom-arrow f g α))) ∙h
( ap-concat-htpy
( map-codomain-hom-arrow f g α ·l F' ∙h coh-hom-arrow f g α)
( right-inv-htpy G ·r map-domain-hom-arrow f g α)) ∙h
( right-unit-htpy) ∙h
( ap-concat-htpy' (coh-hom-arrow f g α) inv-htpy-right-unit-htpy)))

cartesian-hom-arrow-htpy :
{f f' : A → B} (F' : f' ~ f) {g g' : X → Y} (G : g ~ g') →
cartesian-hom-arrow f g → cartesian-hom-arrow f' g'
cartesian-hom-arrow-htpy F' G (α , H) =
( hom-arrow-htpy F' G α , is-cartesian-hom-arrow-htpy F' G α H)


### Cartesian morphisms of arrows are preserved under homotopies of morphisms of arrows

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

abstract
is-cartesian-htpy-hom-arrow :
(α β : hom-arrow f g)
(H : htpy-hom-arrow f g β α) →
is-cartesian-hom-arrow f g α →
is-cartesian-hom-arrow f g β
is-cartesian-htpy-hom-arrow α β H =
is-pullback-htpy
( htpy-codomain-htpy-hom-arrow f g β α H)
( refl-htpy)
( cone-hom-arrow f g α)
( htpy-parallell-cone-htpy-hom-arrow f g β α H)


### The identity cartesian morphism of arrows

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
where

is-cartesian-id-hom-arrow : is-cartesian-hom-arrow f f id-hom-arrow
is-cartesian-id-hom-arrow =
is-pullback-is-equiv-horizontal-maps id f
( f , id , refl-htpy)
( is-equiv-id)
( is-equiv-id)

id-cartesian-hom-arrow : cartesian-hom-arrow f f
id-cartesian-hom-arrow = (id-hom-arrow , is-cartesian-id-hom-arrow)


### Composition of cartesian morphisms of arrows

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
(f : A → B) (g : X → Y) (h : U → V) (b : hom-arrow g h) (a : hom-arrow f g)
where

is-cartesian-comp-hom-arrow :
is-cartesian-hom-arrow g h b →
is-cartesian-hom-arrow f g a →
is-cartesian-hom-arrow f h (comp-hom-arrow f g h b a)
is-cartesian-comp-hom-arrow =
is-pullback-rectangle-is-pullback-left-square
( map-codomain-hom-arrow f g a)
( map-codomain-hom-arrow g h b)
( h)
( cone-hom-arrow g h b)
( cone-hom-arrow f g a)

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
(f : A → B) (g : X → Y) (h : U → V)
(b : cartesian-hom-arrow g h) (a : cartesian-hom-arrow f g)
where

comp-cartesian-hom-arrow : cartesian-hom-arrow f h
comp-cartesian-hom-arrow =
( ( comp-hom-arrow f g h
( hom-arrow-cartesian-hom-arrow g h b)
( hom-arrow-cartesian-hom-arrow f g a)) ,
( is-cartesian-comp-hom-arrow f g h
( hom-arrow-cartesian-hom-arrow g h b)
( hom-arrow-cartesian-hom-arrow f g a)
( is-cartesian-cartesian-hom-arrow g h b)
( is-cartesian-cartesian-hom-arrow f g a)))


### Left cancellation of cartesian morphisms of arrows

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
(f : A → B) (g : X → Y) (h : U → V) (b : hom-arrow g h) (a : hom-arrow f g)
where

is-cartesian-hom-arrow-right-factor :
is-cartesian-hom-arrow g h b →
is-cartesian-hom-arrow f h (comp-hom-arrow f g h b a) →
is-cartesian-hom-arrow f g a
is-cartesian-hom-arrow-right-factor =
is-pullback-left-square-is-pullback-rectangle
( map-codomain-hom-arrow f g a)
( map-codomain-hom-arrow g h b)
( h)
( cone-hom-arrow g h b)
( cone-hom-arrow f g a)


### The left morphism in a commuting triangle of morphisms of arrows is cartesian if the other two are

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
(f : A → B) (g : X → Y) (h : U → V)
(left : hom-arrow f h) (right : hom-arrow g h) (top : hom-arrow f g)
(H : coherence-triangle-hom-arrow f g h left right top)
where

abstract
is-cartesian-left-hom-arrow-triangle :
is-cartesian-hom-arrow g h right →
is-cartesian-hom-arrow f g top →
is-cartesian-hom-arrow f h left
is-cartesian-left-hom-arrow-triangle R T =
is-cartesian-htpy-hom-arrow f h
( comp-hom-arrow f g h right top)
( left)
( H)
( is-cartesian-comp-hom-arrow f g h right top R T)

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
(f : A → B) (g : X → Y) (h : U → V)
(top : cartesian-hom-arrow f g)
(left : hom-arrow f h)
(right : cartesian-hom-arrow g h)
(H :
coherence-triangle-hom-arrow f g h
( left)
( hom-arrow-cartesian-hom-arrow g h right)
( hom-arrow-cartesian-hom-arrow f g top))
where

abstract
is-cartesian-left-cartesian-hom-arrow-triangle :
is-cartesian-hom-arrow f h left
is-cartesian-left-cartesian-hom-arrow-triangle =
is-cartesian-left-hom-arrow-triangle f g h
( left)
( hom-arrow-cartesian-hom-arrow g h right)
( hom-arrow-cartesian-hom-arrow f g top)
( H)
( is-cartesian-cartesian-hom-arrow g h right)
( is-cartesian-cartesian-hom-arrow f g top)


### The top morphism in a commuting triangle of morphisms of arrows is cartesian if the other two are

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
(f : A → B) (g : X → Y) (h : U → V)
(left : hom-arrow f h) (right : hom-arrow g h) (top : hom-arrow f g)
where

abstract
is-cartesian-top-hom-arrow-triangle' :
(H : coherence-triangle-hom-arrow' f g h left right top) →
is-cartesian-hom-arrow g h right →
is-cartesian-hom-arrow f h left →
is-cartesian-hom-arrow f g top
is-cartesian-top-hom-arrow-triangle' H R L =
is-cartesian-hom-arrow-right-factor f g h right top R
( is-cartesian-htpy-hom-arrow f h
( left)
( comp-hom-arrow f g h right top)
( H)
( L))

abstract
is-cartesian-top-hom-arrow-triangle :
(H : coherence-triangle-hom-arrow f g h left right top) →
is-cartesian-hom-arrow g h right →
is-cartesian-hom-arrow f h left →
is-cartesian-hom-arrow f g top
is-cartesian-top-hom-arrow-triangle H =
is-cartesian-top-hom-arrow-triangle'
( inv-htpy-hom-arrow f h left (comp-hom-arrow f g h right top) H)

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
(f : A → B) (g : X → Y) (h : U → V)
(top : hom-arrow f g)
(left : cartesian-hom-arrow f h)
(right : cartesian-hom-arrow g h)
where

abstract
is-cartesian-top-cartesian-hom-arrow-triangle' :
(H :
coherence-triangle-hom-arrow' f g h
( hom-arrow-cartesian-hom-arrow f h left)
( hom-arrow-cartesian-hom-arrow g h right)
( top)) →
is-cartesian-hom-arrow f g top
is-cartesian-top-cartesian-hom-arrow-triangle' H =
is-cartesian-top-hom-arrow-triangle' f g h
( hom-arrow-cartesian-hom-arrow f h left)
( hom-arrow-cartesian-hom-arrow g h right)
( top)
( H)
( is-cartesian-cartesian-hom-arrow g h right)
( is-cartesian-cartesian-hom-arrow f h left)

abstract
is-cartesian-top-cartesian-hom-arrow-triangle :
(H :
coherence-triangle-hom-arrow f g h
( hom-arrow-cartesian-hom-arrow f h left)
( hom-arrow-cartesian-hom-arrow g h right)
( top)) →
is-cartesian-hom-arrow f g top
is-cartesian-top-cartesian-hom-arrow-triangle H =
is-cartesian-top-hom-arrow-triangle f g h
( hom-arrow-cartesian-hom-arrow f h left)
( hom-arrow-cartesian-hom-arrow g h right)
( top)
( H)
( is-cartesian-cartesian-hom-arrow g h right)
( is-cartesian-cartesian-hom-arrow f h left)


### Dependent products of cartesian morphisms of arrows

Given a family of cartesian morphisms of arrows αᵢ : fᵢ → gᵢ, then there is a cartesian morphism of arrows map-Π f → map-Π g.

module _
{l1 l2 l3 l4 l5 : Level}
{I : UU l5} {A : I → UU l1} {B : I → UU l2} {X : I → UU l3} {Y : I → UU l4}
(f : (i : I) → A i → B i) (g : (i : I) → X i → Y i)
(α : (i : I) → cartesian-hom-arrow (f i) (g i))
where

hom-arrow-Π-cartesian-hom-arrow :
hom-arrow (map-Π f) (map-Π g)
hom-arrow-Π-cartesian-hom-arrow =
Π-hom-arrow f g (λ i → hom-arrow-cartesian-hom-arrow (f i) (g i) (α i))

is-cartesian-Π-cartesian-hom-arrow :
is-cartesian-hom-arrow (map-Π f) (map-Π g) hom-arrow-Π-cartesian-hom-arrow
is-cartesian-Π-cartesian-hom-arrow =
is-pullback-Π
( λ i → map-codomain-cartesian-hom-arrow (f i) (g i) (α i))
( g)
( λ i → cone-cartesian-hom-arrow (f i) (g i) (α i))
( λ i → is-cartesian-cartesian-hom-arrow (f i) (g i) (α i))

Π-cartesian-hom-arrow :
cartesian-hom-arrow (map-Π f) (map-Π g)
pr1 Π-cartesian-hom-arrow = hom-arrow-Π-cartesian-hom-arrow
pr2 Π-cartesian-hom-arrow = is-cartesian-Π-cartesian-hom-arrow


### Dependent sums of cartesian morphisms of arrows

Given a family of cartesian morphisms of arrows αᵢ : fᵢ → gᵢ, then there is a cartesian morphism of arrows tot f → tot g.

module _
{l1 l2 l3 l4 l5 : Level}
{I : UU l5} {A : I → UU l1} {B : I → UU l2} {X : I → UU l3} {Y : I → UU l4}
(f : (i : I) → A i → B i) (g : (i : I) → X i → Y i)
(α : (i : I) → cartesian-hom-arrow (f i) (g i))
where

hom-arrow-tot-cartesian-hom-arrow :
hom-arrow (tot f) (tot g)
hom-arrow-tot-cartesian-hom-arrow =
tot-hom-arrow f g (λ i → hom-arrow-cartesian-hom-arrow (f i) (g i) (α i))

is-cartesian-tot-cartesian-hom-arrow :
is-cartesian-hom-arrow (tot f) (tot g) hom-arrow-tot-cartesian-hom-arrow
is-cartesian-tot-cartesian-hom-arrow =
is-pullback-tot-is-pullback-family-id-cone
( λ i → map-codomain-cartesian-hom-arrow (f i) (g i) (α i))
( g)
( λ i → cone-cartesian-hom-arrow (f i) (g i) (α i))
( λ i → is-cartesian-cartesian-hom-arrow (f i) (g i) (α i))

tot-cartesian-hom-arrow :
cartesian-hom-arrow (tot f) (tot g)
pr1 tot-cartesian-hom-arrow = hom-arrow-tot-cartesian-hom-arrow
pr2 tot-cartesian-hom-arrow = is-cartesian-tot-cartesian-hom-arrow


### Cartesian morphisms of arrows are preserved under products

module _
{l1 l2 l3 l4 l5 l6 l7 l8 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
{C : UU l5} {D : UU l6} {Z : UU l7} {W : UU l8}
(f : A → B) (g : X → Y) (h : C → D) (i : Z → W)
(α : cartesian-hom-arrow f g) (β : cartesian-hom-arrow h i)
where

is-cartesian-product-cartesian-hom-arrow :
is-cartesian-hom-arrow
( map-product f h)
( map-product g i)
( product-hom-arrow f g h i
( hom-arrow-cartesian-hom-arrow f g α)
( hom-arrow-cartesian-hom-arrow h i β))
is-cartesian-product-cartesian-hom-arrow =
is-pullback-product-is-pullback
( map-codomain-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α))
( g)
( map-codomain-hom-arrow h i (hom-arrow-cartesian-hom-arrow h i β))
( i)
( cone-cartesian-hom-arrow f g α)
( cone-cartesian-hom-arrow h i β)
( is-cartesian-cartesian-hom-arrow f g α)
( is-cartesian-cartesian-hom-arrow h i β)

product-cartesian-hom-arrow :
cartesian-hom-arrow (map-product f h) (map-product g i)
product-cartesian-hom-arrow =
( ( product-hom-arrow f g h i
( hom-arrow-cartesian-hom-arrow f g α)
( hom-arrow-cartesian-hom-arrow h i β)) ,
( is-cartesian-product-cartesian-hom-arrow))


### Cartesian morphisms of arrows are preserved under coproducts

module _
{l1 l2 l3 l4 l5 l6 l7 l8 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
{C : UU l5} {D : UU l6} {Z : UU l7} {W : UU l8}
(f : A → B) (g : X → Y) (h : C → D) (i : Z → W)
(α : cartesian-hom-arrow f g) (β : cartesian-hom-arrow h i)
where

is-cartesian-coproduct-cartesian-hom-arrow :
is-cartesian-hom-arrow
( map-coproduct f h)
( map-coproduct g i)
( coproduct-hom-arrow f g h i
( hom-arrow-cartesian-hom-arrow f g α)
( hom-arrow-cartesian-hom-arrow h i β))
is-cartesian-coproduct-cartesian-hom-arrow =
is-pullback-coproduct-is-pullback
( map-codomain-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α))
( g)
( map-codomain-hom-arrow h i (hom-arrow-cartesian-hom-arrow h i β))
( i)
( cone-cartesian-hom-arrow f g α)
( cone-cartesian-hom-arrow h i β)
( is-cartesian-cartesian-hom-arrow f g α)
( is-cartesian-cartesian-hom-arrow h i β)

coproduct-cartesian-hom-arrow :
cartesian-hom-arrow (map-coproduct f h) (map-coproduct g i)
coproduct-cartesian-hom-arrow =
( ( coproduct-hom-arrow f g h i
( hom-arrow-cartesian-hom-arrow f g α)
( hom-arrow-cartesian-hom-arrow h i β)) ,
( is-cartesian-coproduct-cartesian-hom-arrow))


### Cartesian morphisms of arrows are preserved under exponentiation

module _
{l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (α : cartesian-hom-arrow f g) (S : UU l5)
where

hom-arrow-postcomp-cartesian-hom-arrow :
hom-arrow (postcomp S f) (postcomp S g)
hom-arrow-postcomp-cartesian-hom-arrow =
postcomp-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α) S

is-cartesian-postcomp-cartesian-hom-arrow :
is-cartesian-hom-arrow
( postcomp S f)
( postcomp S g)
( hom-arrow-postcomp-cartesian-hom-arrow)
is-cartesian-postcomp-cartesian-hom-arrow =
is-pullback-postcomp-is-pullback
( map-codomain-cartesian-hom-arrow f g α)
( g)
( cone-cartesian-hom-arrow f g α)
( is-cartesian-cartesian-hom-arrow f g α)
( S)

postcomp-cartesian-hom-arrow :
cartesian-hom-arrow (postcomp S f) (postcomp S g)
pr1 postcomp-cartesian-hom-arrow =
hom-arrow-postcomp-cartesian-hom-arrow
pr2 postcomp-cartesian-hom-arrow = is-cartesian-postcomp-cartesian-hom-arrow


### A folding operation on cartesian morphisms of arrows

A morphism of arrows

         i
A ------> X
|         |
f |         | g
∨         ∨
B ------> Y
j


is cartesian if and only if either of the folded morphisms

          (f , i)                       (f , i)
A ------> B × X               A ------> B × X
|           |                 |           |
g ∘ i |           | j × g     j ∘ f |           | j × g
∨           ∨                 ∨           ∨
Y ------> Y × Y               Y ------> Y × Y
Δ                             Δ


is.

It remains to formalize the right-hand version.

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

transpose-fold-hom-arrow :
hom-arrow
( λ x → (f x , map-domain-hom-arrow f g α x))
( diagonal-product Y)
transpose-fold-hom-arrow =
hom-arrow-cone
( map-product (map-codomain-hom-arrow f g α) g)
( diagonal-product Y)
( fold-cone (map-codomain-hom-arrow f g α) g (cone-hom-arrow f g α))

fold-hom-arrow :
hom-arrow
( g ∘ map-domain-hom-arrow f g α)
( map-product (map-codomain-hom-arrow f g α) g)
fold-hom-arrow =
transpose-hom-arrow
( λ a → f a , map-domain-hom-arrow f g α a)
( diagonal-product Y)
( transpose-fold-hom-arrow)

is-cartesian-transpose-fold-hom-arrow :
is-cartesian-hom-arrow f g α →
is-cartesian-hom-arrow
( λ x → (f x , map-domain-hom-arrow f g α x))
( diagonal-product Y)
( transpose-fold-hom-arrow)
is-cartesian-transpose-fold-hom-arrow =
is-pullback-fold-cone-is-pullback
( map-codomain-hom-arrow f g α)
( g)
( cone-hom-arrow f g α)

is-cartesian-is-cartesian-transpose-fold-hom-arrow :
is-cartesian-hom-arrow
( λ x → (f x , map-domain-hom-arrow f g α x))
( diagonal-product Y)
( transpose-fold-hom-arrow) →
is-cartesian-hom-arrow f g α
is-cartesian-is-cartesian-transpose-fold-hom-arrow =
is-pullback-is-pullback-fold-cone
( map-codomain-hom-arrow f g α)
( g)
( cone-hom-arrow f g α)

is-cartesian-fold-hom-arrow :
is-cartesian-hom-arrow f g α →
is-cartesian-hom-arrow
( g ∘ map-domain-hom-arrow f g α)
( map-product (map-codomain-hom-arrow f g α) g)
( fold-hom-arrow)
is-cartesian-fold-hom-arrow H =
is-cartesian-transpose-cartesian-hom-arrow
( λ x → (f x , map-domain-hom-arrow f g α x))
( diagonal-product Y)
( transpose-fold-hom-arrow , is-cartesian-transpose-fold-hom-arrow H)

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

transpose-fold-cartesian-hom-arrow :
cartesian-hom-arrow
( λ x → (f x , map-domain-cartesian-hom-arrow f g α x))
( diagonal-product Y)
pr1 transpose-fold-cartesian-hom-arrow =
transpose-fold-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α)
pr2 transpose-fold-cartesian-hom-arrow =
is-cartesian-transpose-fold-hom-arrow f g
( hom-arrow-cartesian-hom-arrow f g α)
( is-cartesian-cartesian-hom-arrow f g α)

fold-cartesian-hom-arrow :
cartesian-hom-arrow
( g ∘ map-domain-cartesian-hom-arrow f g α)
( map-product (map-codomain-cartesian-hom-arrow f g α) g)
pr1 fold-cartesian-hom-arrow =
fold-hom-arrow f g (hom-arrow-cartesian-hom-arrow f g α)
pr2 fold-cartesian-hom-arrow =
is-cartesian-fold-hom-arrow f g
( hom-arrow-cartesian-hom-arrow f g α)
( is-cartesian-cartesian-hom-arrow f g α)


### Lifting cartesian morphisms along lifts of the codomain

Suppose given a cospan of morphisms of arrows

    A ------> C <------ B
|         |       ⌞ |
f |    α    h    β    | g
∨         ∨         ∨
A' -----> C' <----- B'


where β is cartesian. Moreover, suppose we have a map i : A' → B' from the codomain of the source of α to the codomain of the source of β such that the triangle

         i
A' ---> B'
\     /
\   /
∨ ∨
C'


commutes. Then there is a unique morphism of arrows γ : f → g with a homotopy β ~ α ∘ γ extending the triangle, and this morphism is cartesian if and only if α is.

Proof. The unique existence of γ and the homotopy follows from the pullback property of β. The rest is a reiteration of the 3-for-2 property of cartesian morphisms.

We begin by constructing the commuting triangle of morphisms of arrows:

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {A' : UU l2} {B : UU l3} {B' : UU l4} {C : UU l5} {C' : UU l6}
(f : A → A') (g : B → B') (h : C → C')
(β : cartesian-hom-arrow g h)
(α : hom-arrow f h)
(i : A' → B')
(H :
coherence-triangle-maps'
( map-codomain-hom-arrow f h α)
( map-codomain-cartesian-hom-arrow g h β)
( i))
where

cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow :
cone (map-codomain-cartesian-hom-arrow g h β) h A
cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow =
( i ∘ f , map-domain-hom-arrow f h α , H ·r f ∙h coh-hom-arrow f h α)

map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow : A → B
map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow =
gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( is-cartesian-cartesian-hom-arrow g h β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)

hom-arrow-lift-map-codomain-cartesian-hom-arrow : hom-arrow f g
pr1 hom-arrow-lift-map-codomain-cartesian-hom-arrow =
map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow
pr1 (pr2 hom-arrow-lift-map-codomain-cartesian-hom-arrow) = i
pr2 (pr2 hom-arrow-lift-map-codomain-cartesian-hom-arrow) =
inv-htpy
( htpy-vertical-map-gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( is-cartesian-cartesian-hom-arrow g h β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow))

abstract
inv-coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow :
coherence-triangle-hom-arrow' f g h
( α)
( hom-arrow-cartesian-hom-arrow g h β)
( hom-arrow-lift-map-codomain-cartesian-hom-arrow)
inv-coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow =
( htpy-horizontal-map-gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( is-cartesian-cartesian-hom-arrow g h β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)) ,
( H) ,
( ( ap-concat-htpy'
( ( h) ·l
( htpy-horizontal-map-gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( pr2 β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)))
( ap-concat-htpy'
( coh-cartesian-hom-arrow g h β ·r
map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow)
( left-whisker-inv-htpy
( map-codomain-cartesian-hom-arrow g h β)
( htpy-vertical-map-gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( pr2 β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow))))) ∙h
( assoc-htpy
( inv-htpy
( ( map-codomain-cartesian-hom-arrow g h β) ·l
( htpy-vertical-map-gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( pr2 β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow))))
( coh-cartesian-hom-arrow g h β ·r
map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow)
( ( h) ·l
( htpy-horizontal-map-gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( pr2 β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)))) ∙h
( inv-htpy-left-transpose-htpy-concat
( ( map-codomain-cartesian-hom-arrow g h β) ·l
( htpy-vertical-map-gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( pr2 β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)))
( H ·r f ∙h coh-hom-arrow f h α)
( ( coh-cartesian-hom-arrow g h β ·r
map-domain-hom-arrow-lift-map-codomain-cartesian-hom-arrow) ∙h
( h) ·l
( htpy-horizontal-map-gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( is-cartesian-cartesian-hom-arrow g h β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)))
( inv-htpy
( coh-htpy-cone-gap-is-pullback
( map-codomain-cartesian-hom-arrow g h β)
( h)
( cone-cartesian-hom-arrow g h β)
( is-cartesian-cartesian-hom-arrow g h β)
( cone-hom-arrow-lift-map-codomain-cartesian-hom-arrow)))))

coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow :
coherence-triangle-hom-arrow f g h
( α)
( hom-arrow-cartesian-hom-arrow g h β)
( hom-arrow-lift-map-codomain-cartesian-hom-arrow)
coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow =
inv-htpy-hom-arrow f h
( comp-hom-arrow f g h
( hom-arrow-cartesian-hom-arrow g h β)
( hom-arrow-lift-map-codomain-cartesian-hom-arrow))
( α)
( inv-coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow)


Now, if α was cartesian to begin with, the lift is also.

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {A' : UU l2} {B : UU l3} {B' : UU l4} {C : UU l5} {C' : UU l6}
(f : A → A') (g : B → B') (h : C → C')
(β : cartesian-hom-arrow g h)
(α : cartesian-hom-arrow f h)
(i : A' → B')
(H :
coherence-triangle-maps'
( map-codomain-cartesian-hom-arrow f h α)
( map-codomain-cartesian-hom-arrow g h β)
( i))
where

abstract
is-cartesian-cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow :
is-cartesian-hom-arrow f g
( hom-arrow-lift-map-codomain-cartesian-hom-arrow f g h
( β)
( hom-arrow-cartesian-hom-arrow f h α)
( i)
( H))
is-cartesian-cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow =
is-cartesian-top-cartesian-hom-arrow-triangle' f g h
( hom-arrow-lift-map-codomain-cartesian-hom-arrow
( f) g h β (hom-arrow-cartesian-hom-arrow f h α) i H)
( α)
( β)
( inv-coherence-triangle-hom-arrow-lift-map-codomain-cartesian-hom-arrow
( f) g h β (hom-arrow-cartesian-hom-arrow f h α) i H)

cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow :
cartesian-hom-arrow f g
cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow =
( hom-arrow-lift-map-codomain-cartesian-hom-arrow
( f) g h β (hom-arrow-cartesian-hom-arrow f h α) i H) ,
( is-cartesian-cartesian-hom-arrow-lift-map-codomain-cartesian-hom-arrow)