{-# 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
open FreeCategory (CatβGraph π)
semπ = Ξ΅ {π = π}
β¦_β§c = semπ .F-hom
π = PowerCategory (π .ob) (SET (β-max β β'))
π : Functor FreeCat π
π = PseudoYoneda {C = FreeCat}
module YoSem = Semantics π (π βInterp Ξ·)
β¦_β§yo = YoSem.sem .F-hom
eval : β {A B} β FreeCat [ A , B ] β _
eval {A}{B} e = β¦ e β§yo
Yo-YoSem-agree : π β‘ YoSem.sem
Yo-YoSem-agree = YoSem.sem-uniq refl
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