{-
  Arrow category and sub-category of Isos as categories displayed over C × C.

  Universal property: a section of the Arrow bundle is a natural
  transformation between functors, section of the Iso bundle is a
  natural isomorphism

-}
module Cubical.Categories.Displayed.Instances.Arrow where

open import Cubical.Categories.Displayed.Instances.Arrow.Base public