open import Cat.Instances.Elements.Covariant
open import Cat.Functor.Equivalence.Path
open import Cat.Functor.Equivalence
open import Cat.Instances.Product
open import Cat.Prelude

import Cat.Functor.Hom

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

  open Twist

Twist-path
: β {aβ aβ bβ bβ} {f : Hom aβ aβ} {g : Hom bβ bβ} {h1 h2 : Twist f g}
β Twist.before h1 β‘ Twist.before h2
β Twist.after h1 β‘ Twist.after h2
β h1 β‘ h2
Twist-path {h1 = h1} {h2} p q i .Twist.before = p i
Twist-path {h1 = h1} {h2} p q i .Twist.after = q i
Twist-path {h1 = h1} {h2} p q i .Twist.commutes =
is-propβpathp (Ξ» i β Hom-set _ _ (q i β _ β p i) _)
(h1 .Twist.commutes) (h2 .Twist.commutes) i

open Functor

private unquoteDecl eqv = declare-record-iso eqv (quote Twist)

  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

  Twisted .Precategory._β_ {_ , f} {_ , g} {_ , h} t1 t2 .Twist.commutes =
(t1.a β t2.a) β f β t2.b β t1.b β‘β¨ cat! C β©β‘
t1.a β (t2.a β f β t2.b) β t1.b β‘β¨ (Ξ» i β t1.a β t2.commutes i β t1.b) β©β‘
t1.a β g β t1.b                 β‘β¨ t1.commutes β©β‘
h                               β
where
module t1 = Twist t1 renaming (after to a ; before to b)
module t2 = Twist t2 renaming (after to a ; before to b)
Twisted .Precategory.idr f = Twist-path (idl _) (idr _)
Twisted .Precategory.idl f = Twist-path (idr _) (idl _)
Twisted .Precategory.assoc f g h = Twist-path (sym (assoc _ _ _)) (assoc _ _ _)


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 β©οΈ