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

module Cat.Instances.Twisted where


# Twisted arrow categories🔗

The category of arrows of $\mathcal{C}$ is the category ${\mathrm{Arr}}(\mathcal{C})$ which has objects given by morphisms $a_0 {\xrightarrow{a}} a_1 : \mathcal{C}$1, and morphisms $f : a \to b$ given by pairs $f_0, f_1$ as indicated making the diagram below commute.  Now, add a twist. Literally! Invert the direction of the morphism $f_0$ in the definition above. The resulting category is the twisted arrow category of $\mathcal{C}$, written ${\mathrm{Tw}}(\mathcal{C})$. You can think of a morphism $f \to g$ in ${\mathrm{Tw}}(\mathcal{C})$ as a factorisation of $g$ through $f$.

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 ${\mathrm{Tw}}(\mathcal{C}) \to \mathcal{C}{^{{\mathrm{op}}}}\times \mathcal{C}$, which sends each arrow $a {\xrightarrow{f}} b$ to the pair $(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 $(a_0,a_1,a)$ using simply $a$.↩︎