module Cat.Instances.Twisted where

Twisted arrow categoriesπŸ”—

The category of arrows of is the category which has objects given by morphisms 1, and morphisms given by pairs as indicated making the diagram below commute.

Now, add a twist. Literally! Invert the direction of the morphism in the definition above. The resulting category is the twisted arrow category of written You can think of a morphism in as a factorisation of through

module _ {o β„“} (C : Precategory o β„“) where
  open Precategory C
  open Cat.Functor.Hom C

  record Twist {aβ‚€ a₁ bβ‚€ b₁} (f : Hom aβ‚€ a₁) (g : Hom bβ‚€ b₁) : Type β„“ where
    constructor twist
    no-eta-equality
    field
      before : Hom bβ‚€ aβ‚€
      after  : Hom a₁ b₁
      commutes : after ∘ f ∘ before ≑ g
  Twisted : Precategory (o βŠ” β„“) β„“
  Twisted .Precategory.Ob = Ξ£[ (a , b) ∈ Ob Γ— Ob ] Hom a b
  Twisted .Precategory.Hom (_ , f) (_ , g) = Twist f g
  Twisted .Precategory.Hom-set (_ , f) (_ , g) =
    Iso→is-hlevel 2 eqv (hlevel 2)
  Twisted .Precategory.id = record
    { before   = id ; after    = id ; commutes = idl _ βˆ™ idr _ }
  Twisted .Precategory._∘_ t1 t2 .Twist.before = t2 .Twist.before ∘ t1 .Twist.before
  Twisted .Precategory._∘_ t1 t2 .Twist.after   = t1 .Twist.after ∘ t2 .Twist.after

Note that the twisted arrow category is equivalently the covariant category of elements of the Hom functor:

  Twistedβ‰‘βˆ«Hom : Twisted ≑ ∫ Hom[-,-]
  Twistedβ‰‘βˆ«Hom = Precategory-path F F-precat-iso where
    open Element
    open Element-hom
    open is-precat-iso

    F : Functor Twisted (∫ Hom[-,-])
    F .Fβ‚€ a    = elem (a .fst) (a .snd)
    F .F₁ f    = elem-hom (f .before , f .after) (f .commutes)
    F .F-id    = trivial!
    F .F-∘ f g = trivial!

    F-precat-iso : is-precat-iso F
    F-precat-iso .has-is-ff = injective-surjective→is-equiv
      (Element-hom-is-set _ _ _)
      (Ξ» p β†’ Twist-path (ap (fst βŠ™ hom) p) (ap (snd βŠ™ hom) p))
      Ξ» f β†’ inc (twist (f .hom .fst) (f .hom .snd) (f .commute) , trivial!)
    F-precat-iso .has-is-iso = is-iso→is-equiv (iso
      (Ξ» e β†’ e .ob , e .section)
      (Ξ» e β†’ refl) Ξ» e β†’ refl)

The twisted arrow category admits a forgetful functor which sends each arrow to the pair and forgets the commutativity datum for the diagram. Since commutativity of diagrams is a property (rather than structure), this inclusion functor is faithful, though it is not full.

  Ο€β‚œ : Functor Twisted (C ^op Γ—αΆœ C)
  Ο€β‚œ .Fβ‚€   = fst
  Ο€β‚œ .F₁ f = Twist.before f , Twist.after f
  Ο€β‚œ .F-id    = refl
  Ο€β‚œ .F-∘ f g = refl

module _ {o β„“ o' β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'} where
  open Functor
  open Twist

  twistα΅’α΅– : Functor (C ^op Γ—αΆœ C) D β†’ Functor (Twisted (C ^op) ^op) D
  twistα΅’α΅– F .Fβ‚€ ((a , b) , _) = F .Fβ‚€ (a , b)
  twistα΅’α΅– F .F₁ arr  = F .F₁ (arr .before , arr .after)
  twistα΅’α΅– F .F-id    = F .F-id
  twistα΅’α΅– F .F-∘ f g = F .F-∘ _ _

  1. We will metonymically refer to the triple using simply β†©οΈŽ