Double arrows

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2024-04-06.
Last modified on 2026-05-02.

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

open import foundation-core.cartesian-product-types

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

See also

Recent changes