{-# OPTIONS --safe --without-K #-}
 
module CategoricalCrypto.UCSetup where
 
open import Level
open import Relation.Binary.Bundles
 
open import Categories.Category
open import Categories.Category.Instance.Setoids
open import Categories.Category.Monoidal
open import Categories.Functor.Presheaf
open import Categories.Functor.Properties
import Categories.KernelCongruence as KernelCong
open import Categories.Monad.Graded
import Categories.Monad.Graded.Ext as GradedExt
import Categories.Morphism.Reasoning as MR
 
record UCSetup (o ℓ e o′ ℓ′ e′ cs ℓs : Level) : Set (suc (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ cs ⊔ ℓs)) where
  field
    𝒞 : Category o′ ℓ′ e′
    ℐ : MonoidalCategory o ℓ e
    ℳ : GradedKleisliTriple ℐ 𝒞
    ℰ : Presheaf 𝒞 (Setoids cs ℓs)
 
  module 𝒞 where
    open Category 𝒞 public
    open HomReasoning public
    open MR 𝒞 public
  module ℐ = MonoidalCategory ℐ
  open GradedKleisliTriple ℳ public
  open GradedExt ℳ public
  open import Categories.Category.Monoidal.Utilities ℐ.monoidal public
  open Shorthands public
 
  open ℐ using (_⊗₀_; _⊗₁_) public
 
  -- 𝓔-observational equivalence
  module KE = KernelCong 𝒞.op (Setoids cs ℓs) ℰ
 
  open KE using () renaming
    ( _∼_ to _≈ℰ_; ∼-refl to ≈ℰ-refl; ∼-sym to ≈ℰ-sym; ∼-trans to ≈ℰ-trans
    ; ≈⇒∼ to ≈C⇒≈ℰ; ∼-congˡ to ≈ℰ-cong-pre; ∼-congʳ to ≈ℰ-cong-post ) public
 
  ≈ℰ-setoid : (A B : 𝒞.Obj) → Setoid ℓ′ (cs ⊔ ℓs)
  ≈ℰ-setoid A B = KE.∼-setoid B A
 
  GradeStable : Set (o ⊔ o′ ⊔ ℓ′ ⊔ cs ⊔ ℓs)
  GradeStable = ∀ {B C′} (Y : ℐ.Obj) {h h′ : B 𝒞.⇒ C′} → h ≈ℰ h′ → T₁ Y h ≈ℰ T₁ Y h′
 
  -- A faithful ℰ collapses `_≈ℰ_` to 𝒞-equality
  faithful⇒grade-stable : Faithful ℰ → GradeStable
  faithful⇒grade-stable faithful _ e = ≈C⇒≈ℰ (T-resp-≈ (KE.∼⇒≈ faithful e))
 
  -- `GradeStable` whenever the kernel is generated by a conjugation-closed
  -- relation _≋_ and μ has a retraction θ.
  module GradeStableFromTests {r : Level}
    (_≋_ : {A B : 𝒞.Obj} → A 𝒞.⇒ B → A 𝒞.⇒ B → Set r)
    (≋-resp-≈ : {A B : 𝒞.Obj} {f f′ g g′ : A 𝒞.⇒ B}
              → f 𝒞.≈ f′ → g 𝒞.≈ g′ → f ≋ g → f′ ≋ g′)
    (≋-conj : {A B C′ D : 𝒞.Obj} {k : B 𝒞.⇒ C′} {l : D 𝒞.⇒ A} {f g : A 𝒞.⇒ B}
            → f ≋ g → (k 𝒞.∘ f 𝒞.∘ l) ≋ (k 𝒞.∘ g 𝒞.∘ l))
    (≋⇒ℰ : {A B : 𝒞.Obj} {h h′ : A 𝒞.⇒ B}
         → ((V : ℐ.Obj) → T₁ V h ≋ T₁ V h′) → h ≈ℰ h′)
    (ℰ⇒≋ : {A B : 𝒞.Obj} {h h′ : A 𝒞.⇒ B}
         → h ≈ℰ h′ → (V : ℐ.Obj) → T₁ V h ≋ T₁ V h′)
    (θ : {X Y : ℐ.Obj} {A : 𝒞.Obj} → T₀ (X ⊗₀ Y) A 𝒞.⇒ T₀ X (T₀ Y A))
    (θ-μ : {X Y : ℐ.Obj} {A : 𝒞.Obj} → θ 𝒞.∘ μ X Y {A} 𝒞.≈ 𝒞.id)
    where
 
    grade-stable : GradeStable
    grade-stable Z {h} {h′} e =
      ≋⇒ℰ λ Y → ≋-resp-≈ (absorb Y h) (absorb Y h′) (≋-conj (ℰ⇒≋ e (Y ⊗₀ Z)))
      where
      absorb : {A B : 𝒞.Obj} (Y : ℐ.Obj) (k : A 𝒞.⇒ B)
             → θ 𝒞.∘ T₁ (Y ⊗₀ Z) k 𝒞.∘ μ Y Z 𝒞.≈ T₁ Y (T₁ Z k)
      absorb _ _ = let open 𝒞 in (refl⟩∘⟨ ⟺ μ-commute) ○ cancelˡ θ-μ