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

module Categories.Bicategory.Construction.Spans.Properties where

open import Level

open import Data.Product using (_,_; _×_)
open import Function.Bundles using (Func; _⟨$⟩_)
open import Relation.Binary.Bundles using (Setoid)
import Relation.Binary.Reasoning.Setoid as SR

open import Categories.Category.Core using (Category)
open import Categories.Category.Helper using (categoryHelper)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical
  using (pullback; FiberProduct)

open import Categories.Bicategory using (Bicategory)
open import Categories.Bicategory.Monad using (Monad)

import Categories.Category.Diagram.Span as Span
import Categories.Bicategory.Construction.Spans as Spans

--------------------------------------------------------------------------------
-- Monads in the Bicategory of Spans are Categories

module _ {o  : Level} (T : Monad (Spans.Spans (pullback o ))) where

  private
    module T = Monad T

    open Span (Setoids (o  ) )
    open Spans (pullback o )
    open Span⇒
    open Bicategory Spans

    open Setoid renaming (_≈_ to [_][_≈_])
    open Func


  -- We can view the roof of the span as a hom set! However, we need to partition
  -- this big set up into small chunks with known domains/codomains.
  record Hom (X Y : Carrier T.C) : Set (o  ) where
    field
      hom : Carrier (Span.M T.T)
      dom-eq : [ T.C ][ Span.dom T.T ⟨$⟩ hom  X ]
      cod-eq : [ T.C ][ Span.cod T.T ⟨$⟩ hom  Y ]

  open Hom

  private
    ObjSetoid : Setoid (o  ) 
    ObjSetoid = T.C

    HomSetoid : Setoid (o  ) 
    HomSetoid = Span.M T.T

    module ObjSetoid = Setoid ObjSetoid
    module HomSetoid = Setoid HomSetoid

    id⇒ : (X : Carrier T.C)  Hom X X
    id⇒ X = record
      { hom = arr T.η ⟨$⟩ X
      ; dom-eq = commute-dom T.η
      ; cod-eq = commute-cod T.η
      }

    _×ₚ_ :  {A B C}  (f : Hom B C)  (g : Hom A B)  FiberProduct (Span.cod T.T) (Span.dom T.T)
    _×ₚ_ {B = B} f g = record
      { elem₁ = hom g
      ; elem₂ = hom f
      ; commute = begin
        Span.cod T.T ⟨$⟩ hom g ≈⟨ cod-eq g 
        B                      ≈⟨ ObjSetoid.sym (dom-eq f) 
        Span.dom T.T ⟨$⟩ hom f 
      }
      where
        open SR ObjSetoid

    _∘⇒_ :  {A B C} (f : Hom B C)  (g : Hom A B)  Hom A C
    _∘⇒_ {A = A} {C = C} f g = record
      { hom = arr T.μ ⟨$⟩ (f ×ₚ g)
      ; dom-eq = begin
        Span.dom T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ commute-dom T.μ {f ×ₚ g} 
        Span.dom T.T ⟨$⟩ hom g                  ≈⟨ dom-eq g 
        A                                       
      ; cod-eq = begin
        Span.cod T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ commute-cod T.μ {f ×ₚ g} 
        Span.cod T.T ⟨$⟩ hom f                  ≈⟨ cod-eq f 
        C                                       
      }
      where
        open SR ObjSetoid

  SpanMonad⇒Category : Category (o  ) (o  ) 
  SpanMonad⇒Category = categoryHelper record
    { Obj = Setoid.Carrier T.C
    ; _⇒_ = Hom
    ; _≈_ = λ f g  [ HomSetoid ][ hom f  hom g ]
    ; id = λ {X}  id⇒ X
    ; _∘_ = _∘⇒_
    ; assoc = λ {A} {B} {C} {D} {f} {g} {h} 
      let f×ₚ⟨g×ₚh⟩ = record
            { elem₁ = record
              { elem₁ = hom f
              ; elem₂ = hom g
              ; commute = FiberProduct.commute (g ×ₚ f)
              }
            ; elem₂ = hom h
            ; commute = FiberProduct.commute (h ×ₚ g)
            }
      in begin
        arr T.μ ⟨$⟩ ((h ∘⇒ g) ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl)) 
        arr T.μ ⟨$⟩ _                ≈⟨ T.sym-assoc {f×ₚ⟨g×ₚh⟩} 
        arr T.μ ⟨$⟩ _                ≈⟨ (cong (arr T.μ) (cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl) , HomSetoid.refl)) 
        arr T.μ ⟨$⟩ (h ×ₚ (g ∘⇒ f)) 
    ; identityˡ = λ {A} {B} {f}  begin
      arr T.μ ⟨$⟩ (id⇒ B ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.η) (ObjSetoid.sym (cod-eq f))) 
      arr T.μ ⟨$⟩ _             ≈⟨ T.identityʳ 
      hom f                     
    ; identityʳ = λ {A} {B} {f}  begin
      arr T.μ ⟨$⟩ (f ×ₚ id⇒ A) ≈⟨ cong (arr T.μ) (cong (arr T.η) (ObjSetoid.sym (dom-eq f)) , HomSetoid.refl) 
      arr T.μ ⟨$⟩ _             ≈⟨ T.identityˡ 
      hom f                     
    ; equiv = record
      { refl = HomSetoid.refl
      ; sym = HomSetoid.sym
      ; trans = HomSetoid.trans
      }
    ; ∘-resp-≈ = λ f≈h g≈i  Func.cong (arr T.μ) (g≈i , f≈h)
    }
      where
        open SR HomSetoid