Double arrows

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

Created on 2024-04-06.
Last modified on 2024-04-06.

module foundation.double-arrows where
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels


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

    | |
  f | | g
    | |
    ∨ ∨

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.


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)

  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)

  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))

See also

Recent changes