{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category; module Definitions)

-- Definition of the "Twisted Arrow" Category of a Category 𝒞
module Categories.Category.Construction.TwistedArrow {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Data.Product using (_,_; _×_; map; zip)
open import Function.Base using (_$_; flip)
open import Relation.Binary.Core using (Rel)

import Categories.Morphism as M
open M 𝒞
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open Definitions 𝒞
open HomReasoning

private
  variable
    A B C : Obj

record Morphism : Set (o ⊔ ℓ) where
  field
    {dom} : Obj
    {cod} : Obj
    arr   : dom ⇒ cod

record Morphism⇒ (f g : Morphism) : Set (ℓ ⊔ e) where
  constructor mor⇒
  private
    module f = Morphism f
    module g = Morphism g

  field
    {dom⇐} : g.dom ⇒ f.dom
    {cod⇒} : f.cod ⇒ g.cod
    square : cod⇒ ∘ f.arr ∘ dom⇐ ≈ g.arr

TwistedArrow : Category (o ⊔ ℓ) (ℓ ⊔ e) e
TwistedArrow = record
  { Obj       = Morphism
  ; _⇒_       = Morphism⇒
  ; _≈_       = λ f g → dom⇐ f ≈ dom⇐ g × cod⇒ f ≈ cod⇒ g
  ; id        = mor⇒ (identityˡ ○ identityʳ)
  ; _∘_       = λ {A} {B} {C} m₁ m₂ → mor⇒ {A} {C} (∘′ m₁ m₂  ○ square m₁)
  ; assoc     = sym-assoc , assoc
  ; sym-assoc = assoc , sym-assoc
  ; identityˡ = identityʳ , identityˡ
  ; identityʳ = identityˡ , identityʳ
  ; identity² = identity² , identity²
  ; equiv     = record
    { refl  = refl , refl
    ; sym   = map sym sym
    ; trans = zip trans trans
    }
  ; ∘-resp-≈  = zip (flip ∘-resp-≈) ∘-resp-≈
  }
  where
  open Morphism⇒
  open Equiv
  open HomReasoning
  ∘′ : ∀ {A B C} (m₁ : Morphism⇒ B C) (m₂ : Morphism⇒ A B) →
    (cod⇒ m₁ ∘ cod⇒ m₂) ∘ Morphism.arr A ∘ (dom⇐ m₂ ∘ dom⇐ m₁) ≈ cod⇒ m₁ ∘ Morphism.arr B ∘ dom⇐ m₁
  ∘′ {A} {B} {C} m₁ m₂ = begin
    (cod⇒ m₁ ∘ cod⇒ m₂) ∘ Morphism.arr A ∘ (dom⇐ m₂ ∘ dom⇐ m₁) ≈⟨ pullʳ sym-assoc ⟩
    cod⇒ m₁ ∘ (cod⇒ m₂ ∘ Morphism.arr A) ∘ (dom⇐ m₂ ∘ dom⇐ m₁) ≈⟨ refl⟩∘⟨ (pullˡ assoc) ⟩
    cod⇒ m₁ ∘ (cod⇒ m₂ ∘ Morphism.arr A ∘ dom⇐ m₂) ∘ dom⇐ m₁   ≈⟨ (refl⟩∘⟨ square m₂ ⟩∘⟨refl) ⟩
    cod⇒ m₁ ∘ Morphism.arr B ∘ dom⇐ m₁ ∎