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