{-# OPTIONS --without-K --safe #-}

open import Categories.Category using (Category)
open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
open import Function using (flip)
open import Level using (_⊔_)

module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where

module 𝒞 = FinitelyCocompleteCategory 𝒞
open 𝒞 using (U; pushout)
open Category U hiding (_≈_)

open import Categories.Diagram.Pushout U using (Pushout)
open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈; up-to-iso)
open import Relation.Binary using (IsEquivalence)
open import Categories.Morphism U using (_≅_; module ≅)
open import Categories.Morphism.Reasoning U
  using
    ( switch-fromtoˡ
    ; glueTrianglesˡ
    ; pullˡ ; pullʳ
    ; cancelˡ
    )

open import Category.Diagram.Pushout U 
  using
    ( glue-i₁ ; glue-i₂
    ; pushout-f-id ; pushout-id-g
    ; extend-i₁-iso ; extend-i₂-iso
    )

record Cospan (A B : Obj) : Set (o ⊔ ℓ) where

  constructor cospan

  field
    {N} : Obj
    f₁  : A ⇒ N
    f₂  : B ⇒ N

private
  variable
    A B C D : Obj

compose : Cospan A B → Cospan B C → Cospan A C
compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i)
  where
    open pushout g h

identity : Cospan A A
identity = cospan id id

compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D
compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂)
  where
    module P₁ = pushout f₂ g₁
    module P₂ = pushout g₂ h₁
    module P₃ = pushout P₁.i₂ P₂.i₁

record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where

  module C = Cospan C
  module D = Cospan D

  field
    ≅N : C.N ≅ D.N

  open _≅_ ≅N public
  module ≅N = _≅_ ≅N

  field
    from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁
    from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂

private
  variable
    f g h : Cospan A B

≈-refl : f ≈ f
≈-refl {f = cospan f₁ f₂} = record
    { ≅N = ≅.refl
    ; from∘f₁≈f₁ = from∘f₁≈f₁
    ; from∘f₂≈f₂ = from∘f₂≈f₂
    }
  where abstract
    from∘f₁≈f₁ : id ∘ f₁ 𝒞.≈ f₁
    from∘f₁≈f₁ = identityˡ
    from∘f₂≈f₂ : id ∘ f₂ 𝒞.≈ f₂
    from∘f₂≈f₂ = identityˡ

≈-sym : f ≈ g → g ≈ f
≈-sym f≈g = record
    { ≅N = ≅.sym ≅N
    ; from∘f₁≈f₁ = a
    ; from∘f₂≈f₂ = b
    }
  where abstract
    open _≈_ f≈g
    a : ≅N.to ∘ D.f₁ 𝒞.≈ C.f₁
    a = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁)
    b : ≅N.to ∘ D.f₂ 𝒞.≈ C.f₂
    b = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂)

≈-trans : f ≈ g → g ≈ h → f ≈ h
≈-trans f≈g g≈h = record
    { ≅N = ≅.trans f≈g.≅N g≈h.≅N
    ; from∘f₁≈f₁ = a
    ; from∘f₂≈f₂ = b
    }
  where abstract
    module f≈g = _≈_ f≈g
    module g≈h = _≈_ g≈h
    a : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₁ 𝒞.≈ g≈h.D.f₁
    a = glueTrianglesˡ g≈h.from∘f₁≈f₁ f≈g.from∘f₁≈f₁
    b : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₂ 𝒞.≈ g≈h.D.f₂
    b = glueTrianglesˡ g≈h.from∘f₂≈f₂ f≈g.from∘f₂≈f₂

≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B})
≈-equiv = record
    { refl = ≈-refl
    ; sym = ≈-sym
    ; trans = ≈-trans
    }

compose-idˡ : compose f identity ≈ f
compose-idˡ {f = cospan {N} f₁ f₂} = record
    { ≅N = ≅P
    ; from∘f₁≈f₁ = from∘f₁≈f₁
    ; from∘f₂≈f₂ = from∘f₂≈f₂
    }
  where
    open HomReasoning
    P P′ : Pushout f₂ id
    P = pushout f₂ id
    P′ = pushout-f-id {f = f₂}
    module P = Pushout P
    ≅P : P.Q ≅ N
    ≅P = up-to-iso P P′
    module ≅P = _≅_ ≅P
    abstract
      from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ f₁ 𝒞.≈ f₁
      from∘f₁≈f₁ = begin
          ≅P.from ∘ P.i₁ ∘ f₁ ≈⟨ cancelˡ P.universal∘i₁≈h₁ ⟩
          f₁                  ∎
      from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ id 𝒞.≈ f₂
      from∘f₂≈f₂ = begin
          ≅P.from ∘ P.i₂ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩
          ≅P.from ∘ P.i₂      ≈⟨ P.universal∘i₂≈h₂ ⟩
          f₂                  ∎

compose-idʳ : compose identity f ≈ f
compose-idʳ {f = cospan {N} f₁ f₂} = record
    { ≅N = ≅P
    ; from∘f₁≈f₁ = from∘f₁≈f₁
    ; from∘f₂≈f₂ = from∘f₂≈f₂
    }
  where
    open HomReasoning
    P P′ : Pushout id f₁
    P = pushout id f₁
    module P = Pushout P
    P′ = pushout-id-g {g = f₁}
    ≅P : P.Q ≅ N
    ≅P = up-to-iso P P′
    module ≅P = _≅_ ≅P
    abstract
      from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ id 𝒞.≈ f₁
      from∘f₁≈f₁ = begin
          ≅P.from ∘ P.i₁ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩
          ≅P.from ∘ P.i₁      ≈⟨ P.universal∘i₁≈h₁ ⟩
          f₁                  ∎
      from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ f₂ 𝒞.≈ f₂
      from∘f₂≈f₂ = begin
          ≅P.from ∘ P.i₂ ∘ f₂ ≈⟨ cancelˡ P.universal∘i₂≈h₂ ⟩
          f₂                  ∎

compose-id² : compose identity identity ≈ identity {A}
compose-id² = compose-idˡ

compose-3-right : compose f (compose g h) ≈ compose-3 f g h
compose-3-right {f = f} {g = g} {h = h} = record
    { ≅N = ≅N
    ; from∘f₁≈f₁ = from∘f₁≈f₁
    ; from∘f₂≈f₂ = from∘f₂≈f₂
    }
  where
    open HomReasoning
    module C₁ = Cospan f
    module C₂ = Cospan g
    module C₃ = Cospan h
    P₁ : Pushout C₁.f₂ C₂.f₁
    P₁ = pushout C₁.f₂ C₂.f₁
    P₂ : Pushout C₂.f₂ C₃.f₁
    P₂ = pushout C₂.f₂ C₃.f₁
    module P₁ = Pushout P₁
    module P₂ = Pushout P₂
    P₃ : Pushout P₁.i₂ P₂.i₁
    P₃ = pushout P₁.i₂ P₂.i₁
    module P₃ = Pushout P₃
    P₄ P₄′ : Pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁)
    P₄ = glue-i₂ P₁ P₃
    P₄′ = pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁)
    module P₄ = Pushout P₄
    module P₄′ = Pushout P₄′
    ≅N : P₄′.Q ≅ P₄.Q
    ≅N = up-to-iso P₄′ P₄
    module ≅N = _≅_ ≅N
    abstract
      from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ C₁.f₁ 𝒞.≈ P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁
      from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc
      from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ P₂.i₂ ∘ C₃.f₂ 𝒞.≈ P₄.i₂ ∘ P₂.i₂ ∘ C₃.f₂
      from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl

compose-3-left : compose (compose f g) h ≈ compose-3 f g h
compose-3-left {f = f} {g = g} {h = h} = record
    { ≅N = up-to-iso P₄′ P₄
    ; from∘f₁≈f₁ = from∘f₁≈f₁
    ; from∘f₂≈f₂ = from∘f₂≈f₂
    }
  where
    open HomReasoning
    module C₁ = Cospan f
    module C₂ = Cospan g
    module C₃ = Cospan h
    P₁ : Pushout C₁.f₂ C₂.f₁
    P₁ = pushout C₁.f₂ C₂.f₁
    P₂ : Pushout C₂.f₂ C₃.f₁
    P₂ = pushout C₂.f₂ C₃.f₁
    module P₁ = Pushout P₁
    module P₂ = Pushout P₂
    P₃ : Pushout P₁.i₂ P₂.i₁
    P₃ = pushout P₁.i₂ P₂.i₁
    module P₃ = Pushout P₃
    P₄ P₄′ : Pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁
    P₄ = glue-i₁ P₂ P₃
    P₄′ = pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁
    module P₄ = Pushout P₄
    module P₄′ = Pushout P₄′
    ≅N : P₄′.Q ≅ P₄.Q
    ≅N = up-to-iso P₄′ P₄
    module ≅N = _≅_ ≅N
    abstract
      from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ P₁.i₁ ∘ C₁.f₁ 𝒞.≈ P₄.i₁ ∘ P₁.i₁ ∘ C₁.f₁
      from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl
      from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ C₃.f₂ 𝒞.≈ P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂
      from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc

compose-assoc
    : {c₁ : Cospan A B}
      {c₂ : Cospan B C}
      {c₃ : Cospan C D}
    → compose c₁ (compose c₂ c₃) ≈ (compose (compose c₁ c₂) c₃)
compose-assoc = ≈-trans compose-3-right (≈-sym compose-3-left)

compose-sym-assoc
    : {c₁ : Cospan A B}
      {c₂ : Cospan B C}
      {c₃ : Cospan C D}
    → compose (compose c₁ c₂) c₃ ≈ compose c₁ (compose c₂ c₃)
compose-sym-assoc = ≈-trans compose-3-left (≈-sym compose-3-right)

compose-equiv
    : {c₂ c₂′ : Cospan B C}
      {c₁ c₁′ : Cospan A B}
    → c₂ ≈ c₂′
    → c₁ ≈ c₁′
    → compose c₁ c₂ ≈ compose c₁′ c₂′
compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≈C₂ ≈C₁ = record
    { ≅N = ≅P
    ; from∘f₁≈f₁ = from∘f₁≈f₁
    ; from∘f₂≈f₂ = from∘f₂≈f₂
    }
  where
    module C₁ = Cospan c₁
    module C₁′ = Cospan c₁′
    module C₂ = Cospan c₂
    module C₂′ = Cospan c₂′
    P : Pushout C₁.f₂ C₂.f₁
    P = pushout C₁.f₂ C₂.f₁
    P′ : Pushout C₁′.f₂ C₂′.f₁
    P′ = pushout C₁′.f₂ C₂′.f₁
    module ≈C₁ = _≈_ ≈C₁
    module ≈C₂ = _≈_ ≈C₂
    P′′ : Pushout (≈C₁.to ∘ C₁′.f₂) (≈C₂.to ∘ C₂′.f₁)
    P′′ = extend-i₂-iso (extend-i₁-iso P′ (≅.sym ≈C₁.≅N)) (≅.sym ≈C₂.≅N)
    P″ : Pushout C₁.f₂ C₂.f₁
    P″ =
        pushout-resp-≈
            P′′
            (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂))
            (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁))
    module P = Pushout P
    module P′ = Pushout P′
    ≅P : P.Q ≅ P′.Q
    ≅P = up-to-iso P P″
    module ≅P = _≅_ ≅P
    open HomReasoning
    abstract
      from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ C₁.f₁ 𝒞.≈ P′.i₁ ∘ C₁′.f₁
      from∘f₁≈f₁ = begin
          ≅P.from ∘ P.i₁ ∘ C₁.f₁      ≈⟨ pullˡ P.universal∘i₁≈h₁ ⟩
          (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁  ≈⟨ pullʳ ≈C₁.from∘f₁≈f₁ ⟩
          P′.i₁ ∘ C₁′.f₁              ∎
      from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ C₂.f₂ 𝒞.≈ P′.i₂ ∘ C₂′.f₂
      from∘f₂≈f₂ = begin
          ≅P.from ∘ P.i₂ ∘ C₂.f₂      ≈⟨ pullˡ P.universal∘i₂≈h₂ ⟩
          (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂  ≈⟨ pullʳ ≈C₂.from∘f₂≈f₂ ⟩
          P′.i₂ ∘ C₂′.f₂              ∎

Cospans : Category o (o ⊔ ℓ) (ℓ ⊔ e)
Cospans = record
    { Obj = Obj
    ; _⇒_ = Cospan
    ; _≈_ = _≈_
    ; id = identity
    ; _∘_ = flip compose
    ; assoc = compose-assoc
    ; sym-assoc = compose-sym-assoc
    ; identityˡ = compose-idˡ
    ; identityʳ = compose-idʳ
    ; identity² = compose-id²
    ; equiv = ≈-equiv
    ; ∘-resp-≈ = compose-equiv
    }