open import Cat.Instances.Product
open import Cat.Prelude

module Cat.Instances.Twisted where

Twisted arrow categoriesπŸ”—

The category of arrows of C\mathcal{C} is the category Arr(C){\mathrm{Arr}}(\mathcal{C}) which has objects given by morphisms a0→aa1:Ca_0 {\xrightarrow{a}} a_1 : \mathcal{C}1, and morphisms f:a→bf : a \to b given by pairs f0,f1f_0, f_1 as indicated making the diagram below commute.

Now, add a twist. Literally! Invert the direction of the morphism f0f_0 in the definition above. The resulting category is the twisted arrow category of C\mathcal{C}, written Tw(C){\mathrm{Tw}}(\mathcal{C}). You can think of a morphism f→gf \to g in Tw(C){\mathrm{Tw}}(\mathcal{C}) as a factorisation of gg through ff.

module _ {o β„“} {C : Precategory o β„“} where
  open Precategory C
  record Twist {aβ‚€ a₁ bβ‚€ b₁} (f : Hom aβ‚€ a₁) (g : Hom bβ‚€ b₁) : Type β„“ where
    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

The twisted arrow category admits a forgetful functor Tw(C)→Cop×C{\mathrm{Tw}}(\mathcal{C}) \to \mathcal{C}{^{{\mathrm{op}}}}\times \mathcal{C}, which sends each arrow a→fba {\xrightarrow{f}} b to the pair (a,b)(a, b), 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
  twistα΅’α΅– : Functor (C ^op Γ—αΆœ C) D β†’ Functor (Twisted {C = C ^op} ^op) D
  twistα΅’α΅– F .Functor.Fβ‚€ ((a , b) , _) = F .Functor.Fβ‚€ (a , b)
  twistα΅’α΅– F .Functor.F₁ arr = F .Functor.F₁ (Twist.before arr , Twist.after arr)
  twistα΅’α΅– F .Functor.F-id = F .Functor.F-id
  twistα΅’α΅– F .Functor.F-∘ f g = F .Functor.F-∘ _ _

  1. We will metonymically refer to the triple (a0,a1,a)(a_0,a_1,a) using simply aa.β†©οΈŽ