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
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 $\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$.↩︎