search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
25 stars 5 forks source link

Category Solver Bug? #20

Closed stschaef closed 1 year ago

stschaef commented 1 year ago

Unsure if this is a bug or if I'm just using the cat solver in a sketchy spot

Trying to show equivalence of the different notions of cones. The following does not work, and gives a levels issue at the ×F term. However, if you uncomment the additional refl it goes through.

My initial thought is that solveCat! C should behave the same on definitionally equal terms, but maybe there is some reflection weirdness going on here

    Cone→CONE : Cone D c → (CONE ⟅ c , D ⟆) .fst
    Cone→CONE record-cone .N-ob x =  record-cone .coneOut x
    Cone→CONE record-cone .N-hom {x}{y} f = 
      (fst (((λFr J C (Fst C J) ^opF) ×F Id) ⟅ c , D ⟆) .F-hom f
        ⋆⟨ C ⟩
        record-cone .coneOut y)
--        ≡⟨ refl ⟩
--    Constant J C c .F-hom f ⋆⟨ C ⟩ record-cone .coneOut y
        ≡⟨ solveCat! C ⟩
          record-cone .coneOut y
        ≡⟨ sym (record-cone .coneOutCommutes f) ⟩
      (record-cone .coneOut x
        ⋆⟨ C ⟩
        snd (((λFr J C (Fst C J) ^opF) ×F Id) ⟅ c , D ⟆) .F-hom f) ∎
maxsnew commented 1 year ago

Because it uses reflection, the solver definitely does not respect definitional equality. It tries to parse the goal without normalizing calls to Category._*_ and Category.id. No idea what's going on in this particular case tho

stschaef commented 1 year ago

Ah, that makes sense

Closing this non-bug then