{-# OPTIONS --without-K #-}
module Model.RGraph where

open import Cats.Category
open import Relation.Binary using (IsEquivalence)

open import Util.HoTT.Equiv
open import Util.HoTT.FunctionalExtensionality
open import Util.HoTT.HLevel
open import Util.Prelude hiding (id) renaming (_∘_ to _∘F_)
open import Util.Relation.Binary.PropositionalEquality


infixr 0 _⇒_
infix 4 _≈_
infixr 9 _∘_


record RGraph : Set₁ where
  no-eta-equality
  field
    ObjHSet : HSet 0ℓ

  open HLevel ObjHSet public using () renaming
    ( type to Obj
    ; level to Obj-IsSet
    )

  field
    eqHProp : Obj  Obj  HProp 0ℓ

  private
    module M₀ x y = HLevel (eqHProp x y)
    module M₁ {x} {y} = HLevel (eqHProp x y)

  open M₀ public using () renaming
    ( type to eq )
  open M₁ public using () renaming
    ( level to eq-IsProp )

  field
    eq-refl :  x  eq x x

open RGraph public


private
  variable Γ Δ Ψ : RGraph


record _⇒_ (Γ Δ : RGraph) : Set where
  no-eta-equality
  field
    fobj : Γ .Obj  Δ .Obj
    feq :  {x y}  Γ .eq x y  Δ .eq (fobj x) (fobj y)

open _⇒_ public


private
  variable f g h i : Γ  Δ


⇒Canon : (Γ Δ : RGraph)  Set
⇒Canon Γ Δ
  = Σ[ fobj  (Γ .Obj  Δ .Obj) ]
      (∀ {x y}  Γ .eq x y  Δ .eq (fobj x) (fobj y))


⇒≅⇒Canon : (Γ  Δ)  (⇒Canon Γ Δ)
⇒≅⇒Canon = record
  { forth = λ f  f .fobj , f .feq
  ; isIso = record
    { back = λ f  record { fobj = proj₁ f ; feq = proj₂ f }
    ; back∘forth = λ where
        record { fobj = fobj ; feq = feq }  refl
    ; forth∘back = λ f  refl
    }
  }


⇒Canon-IsSet :  Γ Δ  IsSet (⇒Canon Γ Δ)
⇒Canon-IsSet Γ Δ
  = Σ-IsSet
      (→-IsSet (Δ .Obj-IsSet))
       _  ∀∙-IsSet  _  ∀∙-IsSet λ _  →-IsSet (IsProp→IsSet (Δ .eq-IsProp))))


⇒-IsSet : IsSet (Γ  Δ)
⇒-IsSet {Γ} {Δ} = ≅-pres-IsOfHLevel 2 (≅-sym ⇒≅⇒Canon) (⇒Canon-IsSet Γ Δ)


record _≈_ (f g : Γ  Δ) : Set where
  no-eta-equality
  constructor ≈⁺
  field
    ≈⁻ :  x  f .fobj x  g .fobj x

open _≈_ public


≈→≡Canon :  {Γ Δ} {f g : Γ  Δ}
   f  g
   ⇒≅⇒Canon .forth f  ⇒≅⇒Canon .forth g
≈→≡Canon {Δ = Δ} {f} {g} (≈⁺ f≈g) = Σ-≡⁺
  ( funext f≈g
  , funext∙ (funext∙ (funext λ x≈y  Δ .eq-IsProp _ _))
  )


≈→≡ : f  g  f  g
≈→≡ f≈g = ≅-Injective ⇒≅⇒Canon (≈→≡Canon f≈g)


≈-isEquivalence :  Γ Δ  IsEquivalence (_≈_ {Γ} {Δ})
≈-isEquivalence Γ Δ = record
  { refl = ≈⁺  x  refl)
  ; sym = λ f≈g  ≈⁺  x  sym (f≈g .≈⁻ x))
  ; trans = λ f≈g g≈h  ≈⁺  x  trans (f≈g .≈⁻ x) (g≈h .≈⁻ x))
  }


private
  open module M₀ {Γ} {Δ}
    = IsEquivalence (≈-isEquivalence Γ Δ) public using () renaming
    ( refl to ≈-refl
    ; sym to ≈-sym
    ; trans to ≈-trans
    ; reflexive to ≈-reflexive )


id :  {Γ}  Γ  Γ
id = record { fobj = λ x  x ; feq = λ x  x }


_∘_ :  {Γ Δ Ψ}  Δ  Ψ  Γ  Δ  Γ  Ψ
f  g = record
  { fobj = f .fobj ∘F g .fobj
  ; feq = f .feq ∘F g .feq
  }


RGraphs : Category (lsuc 0ℓ) 0ℓ 0ℓ
RGraphs = record
  { Obj = RGraph
  ; _⇒_ = _⇒_
  ; _≈_ = _≈_
  ; id = id
  ; _∘_ = _∘_
  ; equiv = ≈-isEquivalence _ _
  ; ∘-resp = λ {Γ Δ Ψ f g h i} f≈g h≈i
       ≈⁺  x  trans (f≈g .≈⁻ _) (cong (g .fobj) (h≈i .≈⁻ x)))
  ; id-r = ≈⁺  x  refl)
  ; id-l = ≈⁺  x  refl)
  ; assoc = ≈⁺  x  refl)
  }


module RGraphs = Category RGraphs