{-# OPTIONS --safe --lossy-unification #-}
module Cubical.Tactics.CategorySolver.Solver where

open import Cubical.Foundations.Prelude

open import Cubical.Categories.Category
open import Cubical.Categories.Constructions.Free.Category.Base
open import Cubical.Categories.Constructions.Power
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.UnderlyingGraph

private
  variable
    β„“ β„“' : Level
open Category
open Functor

module Eval (𝓒 : Category β„“ β„“') where
  -- Semantics in 𝓒 itself, tautologically
  open FreeCategory (Catβ†’Graph 𝓒)
  sem𝓒 = Ξ΅ {𝓒 = 𝓒}
  ⟦_⟧c = sem𝓒 .F-hom
  π“Ÿ = PowerCategory (𝓒 .ob) (SET (β„“-max β„“ β„“'))
  π“˜ : Functor FreeCat π“Ÿ
  π“˜ = PseudoYoneda {C = FreeCat}

  -- Semantics in π“Ÿ (𝓒 .ob), interpreting fun symbols using Yoneda
  module YoSem = Semantics π“Ÿ (π“˜ ∘Interp Ξ·)
  ⟦_⟧yo = YoSem.sem .F-hom

  -- | Evaluate by taking the semantics in π“Ÿ (𝓒 .ob)
  eval : βˆ€ {A B} β†’ FreeCat [ A , B ] β†’ _
  eval {A}{B} e = ⟦ e ⟧yo

  -- Evaluation agrees with the Yoneda embedding, and so is fully faithful
  Yo-YoSem-agree : π“˜ ≑ YoSem.sem
  Yo-YoSem-agree = YoSem.sem-uniq refl

  -- If two expressions in the free category are equal when evaluated
  -- in π“Ÿ (𝓒 .ob), then they are equal, and so are equal when
  -- evaluated in 𝓒.
  solve : βˆ€ {A B} β†’ (e₁ eβ‚‚ : FreeCat [ A , B ])
        β†’ eval e₁ ≑ eval eβ‚‚
        β†’ ⟦ e₁ ⟧c ≑ ⟦ eβ‚‚ ⟧c
  solve {A}{B} e₁ eβ‚‚ p = cong ⟦_⟧c (isFaithfulPseudoYoneda _ _ _ _ lem) where
    lem : π“˜ βŸͺ e₁ ⟫ ≑ π“˜ βŸͺ eβ‚‚ ⟫
    lem = transport
            (Ξ» i β†’ Yo-YoSem-agree (~ i) βŸͺ e₁ ⟫ ≑ Yo-YoSem-agree (~ i) βŸͺ eβ‚‚ ⟫)
            p

solve : (𝓒 : Category β„“ β„“')
      β†’ {A B : 𝓒 .ob}
      β†’ (e₁ eβ‚‚ : FreeCategory.FreeCat (Catβ†’Graph 𝓒) [ A , B ])
      β†’ (p : Eval.eval 𝓒 e₁ ≑ Eval.eval 𝓒 eβ‚‚)
      β†’ _
solve = Eval.solve