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 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
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 _ _ _)
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 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-β _ _
We will metonymically refer to the triple using simply .β©οΈ