# Morphisms of twisted arrows

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-09.

module foundation.morphisms-twisted-arrows where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.homotopies


## Idea

A morphism of twisted arrows from f : A → B to g : X → Y is a triple (i , j , H) consisting of

• a map i : X → A

• a map j : B → Y, and

• a homotopy H : j ∘ f ∘ i ~ g witnessing that the square

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


commutes.

Thus, a morphism of twisted arrows can also be understood as a factorization of g through f.

## Definitions

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

coherence-hom-twisted-arrow :
(X → A) → (B → Y) → UU (l3 ⊔ l4)
coherence-hom-twisted-arrow i j = j ∘ f ∘ i ~ g

hom-twisted-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
hom-twisted-arrow =
Σ (X → A) (λ i → Σ (B → Y) (coherence-hom-twisted-arrow i))

module _
(α : hom-twisted-arrow)
where

map-domain-hom-twisted-arrow : X → A
map-domain-hom-twisted-arrow = pr1 α

map-codomain-hom-twisted-arrow : B → Y
map-codomain-hom-twisted-arrow = pr1 (pr2 α)

coh-hom-twisted-arrow :
map-codomain-hom-twisted-arrow ∘ f ∘ map-domain-hom-twisted-arrow ~ g
coh-hom-twisted-arrow = pr2 (pr2 α)