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}$¹, 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
    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  eqv (hlevel )
  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 $\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-∘ _ _