Model.RGraph

{-# 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