# Double arrows

Content created by Vojtěch Štěpančík.

Created on 2024-04-06.

module foundation.double-arrows where

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


## Idea

A double arrow is a pair of types A, B equipped with a pair of maps f, g : A → B.

We draw a double arrow as

     A
| |
f | | g
| |
∨ ∨
B


where f is the first map in the structure and g is the second map in the structure. We also call f the left map and g the right map. By convention, homotopies go from left to right.

## Definitions

### Double arrows

double-arrow : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
double-arrow l1 l2 = Σ (UU l1) (λ A → Σ (UU l2) (λ B → (A → B) × (A → B)))

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

make-double-arrow : double-arrow l1 l2
make-double-arrow = (A , B , f , g)

{-# INLINE make-double-arrow #-}


### Components of a double arrow

module _
{l1 l2 : Level} (a : double-arrow l1 l2)
where

domain-double-arrow : UU l1
domain-double-arrow = pr1 a

codomain-double-arrow : UU l2
codomain-double-arrow = pr1 (pr2 a)

left-map-double-arrow : domain-double-arrow → codomain-double-arrow
left-map-double-arrow = pr1 (pr2 (pr2 a))

right-map-double-arrow : domain-double-arrow → codomain-double-arrow
right-map-double-arrow = pr2 (pr2 (pr2 a))