New version of Free Functor (#49)

* prove uniqueness property for functors/sections out of a free cat
* reformulate Free Functor to use Presented Cat, define elim w/o Eq!
* Implement kernel of new functor solver using displayed cats (still need new parser)
* Move Quiver to Data.Quiver, define Graph^D over Quiver
* Reformulate Presented Cat to take in a category rather than quiver
* fix github workflow

.github/workflows/main.yml

@@ -54,8 +54,8 @@ on:
 ########################################################################
 
 env:
-  AGDA_BRANCH: v2.6.3
-  GHC_VERSION: 9.2.5
+  AGDA_BRANCH: v2.6.4
+  GHC_VERSION: 9.4.7
   CABAL_VERSION: 3.6.2.0
   CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
   CACHE_PATHS: |

Cubical/Categories/Constructions/BinProduct/Redundant/Assoc.agda

@@ -19,7 +19,7 @@ import Cubical.Categories.Constructions.BinProduct.Redundant.Assoc.ToLeft
 open import Cubical.Categories.Constructions.BinProduct.Redundant.Base as BP
 open import Cubical.Categories.Constructions.Free.Category.Quiver as Free
   hiding (rec)
-open import Cubical.Categories.Constructions.Presented as Presented hiding (rec)
+open import Cubical.Categories.Constructions.Presented as Presented
 open import Cubical.Categories.Bifunctor.Redundant
 
 private

Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToLeft.agda

@@ -15,7 +15,7 @@ open import Cubical.Data.Sigma
 open import Cubical.Categories.Constructions.BinProduct.Redundant.Base as BP
 open import Cubical.Categories.Constructions.Free.Category.Quiver as Free
   hiding (rec)
-open import Cubical.Categories.Constructions.Presented as Presented hiding (rec)
+open import Cubical.Categories.Constructions.Presented as Presented
 open import Cubical.Categories.Bifunctor.Redundant as Bif
 
 private
@@ -25,7 +25,6 @@ private
 open Category
 open Functor
 open NatTrans
-open Interpᴰ
 open Axioms
 open Bifunctor
 open BifunctorParAx

Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToRight.agda

@@ -15,7 +15,7 @@ open import Cubical.Data.Sigma
 open import Cubical.Categories.Constructions.BinProduct.Redundant.Base as BP
 open import Cubical.Categories.Constructions.Free.Category.Quiver as Free
   hiding (rec)
-open import Cubical.Categories.Constructions.Presented as Presented hiding (rec)
+open import Cubical.Categories.Constructions.Presented as Presented
 open import Cubical.Categories.Bifunctor.Redundant
 
 private
@@ -25,7 +25,6 @@ private
 open Category
 open Functor
 open NatTrans
-open Interpᴰ
 open Axioms
 open Bifunctor
 open BifunctorParAx

Cubical/Categories/Constructions/BinProduct/Redundant/Base.agda

@@ -13,11 +13,12 @@ open import Cubical.Categories.NaturalTransformation
 open import Cubical.Data.Graph.Base
 open import Cubical.Data.Sum as Sum hiding (rec)
 open import Cubical.Data.Sigma
+open import Cubical.Data.Quiver.Base
 
 import Cubical.Categories.Constructions.BinProduct as BP
 open import Cubical.Categories.Constructions.Free.Category.Quiver as Free
   hiding (rec)
-open import Cubical.Categories.Constructions.Presented as Presented hiding (rec)
+open import Cubical.Categories.Constructions.Presented as Presented
 open import Cubical.Categories.Bifunctor.Redundant
 
 private
@@ -27,7 +28,6 @@ private
 open Category
 open Functor
 open QuiverOver
-open Interpᴰ
 open Axioms
 
 module _ (C : Category ℓc ℓc') (D : Category ℓd ℓd') where
@@ -58,20 +58,26 @@ module _ (C : Category ℓc ℓc') (D : Category ℓd ℓd') where
     Q .snd .dom (hom× {c = c}{d = d} f g) = c , d
     Q .snd .cod (hom× {c' = c'}{d' = d'} f g) = c' , d'
 
-    Ax : Axioms Q (ℓ-max (ℓ-max ℓc ℓc') (ℓ-max ℓd ℓd'))
-    Ax = mkAx Q ProdAx λ
+    Ax : Axioms (FreeCat Q) (ℓ-max (ℓ-max ℓc ℓc') (ℓ-max ℓd ℓd'))
+    Ax = mkAx (FreeCat Q) ProdAx λ
       { (×-id c d) → _ , _ ,
-        η Q .I-hom (hom× (C .id {c}) (D .id {d}))
+        η Q <$g> (hom× (C .id {c}) (D .id {d}))
         , FreeCat Q .id
       ; (×-seq f f' g g') → _ , _ ,
-        η Q .I-hom (hom× (f ⋆⟨ C ⟩ f') (g ⋆⟨ D ⟩ g'))
-        , ((η Q .I-hom (hom× f g)) ⋆⟨ FreeCat Q ⟩ (η Q .I-hom (hom× f' g')))
+        η Q <$g> (hom× (f ⋆⟨ C ⟩ f') (g ⋆⟨ D ⟩ g'))
+        , ((η Q <$g> (hom× f g)) ⋆⟨ FreeCat Q ⟩ (η Q <$g> (hom× f' g')))
       ; (L×-agree f d) → _ , _ ,
-        η Q .I-hom (homL f d) , η Q .I-hom (hom× f (D .id {d}))
+        η Q <$g> (homL f d) , η Q <$g> (hom× f (D .id {d}))
       ; (R×-agree c g) → _ , _ ,
-        η Q .I-hom (homR c g) , η Q .I-hom (hom× (C .id {c}) g) }
+        η Q <$g> (homR c g) , η Q <$g> (hom× (C .id {c}) g) }
+
+  module ProdCat = QuoByAx (FreeCat Q) Ax
   _×C_ : Category (ℓ-max ℓc ℓd) (ℓ-max (ℓ-max ℓc ℓc') (ℓ-max ℓd ℓd'))
-  _×C_ = PresentedCat Q Ax
+  _×C_ = ProdCat.PresentedCat
+
+  private
+    ηMor : ∀ (e : Q .snd .mor) → _×C_ [ _ , _ ]
+    ηMor e = ProdCat.ToPresented ⟪ η Q <$g> e ⟫
 
   open Bifunctor
 
@@ -82,27 +88,27 @@ module _ (C : Category ℓc ℓc') (D : Category ℓd ℓd') where
       open BifunctorParAx
       η' : BifunctorParAx C D _×C_
       η' .Bif-ob = _,_
-      η' .Bif-homL f d = ηP Q Ax .I-hom (homL f d)
-      η' .Bif-homR c g = ηP Q Ax .I-hom (homR c g)
-      η' .Bif-hom× f g = ηP Q Ax .I-hom (hom× f g)
-      η' .Bif-×-id = ηEq Q Ax (×-id _ _)
-      η' .Bif-×-seq f f' g g' = ηEq Q Ax (×-seq f f' g g')
-      η' .Bif-L×-agree f = ηEq Q Ax (L×-agree f _)
-      η' .Bif-R×-agree g = ηEq Q Ax (R×-agree _ g)
+      η' .Bif-homL f d = ηMor (homL f d)
+      η' .Bif-homR c g = ηMor (homR c g)
+      η' .Bif-hom× f g = ηMor (hom× f g)
+      η' .Bif-×-id = ProdCat.ηEq (×-id _ _)
+      η' .Bif-×-seq f f' g g' = ProdCat.ηEq (×-seq f f' g g')
+      η' .Bif-L×-agree f = ProdCat.ηEq (L×-agree f _)
+      η' .Bif-R×-agree g = ProdCat.ηEq (R×-agree _ g)
 
   rec : {E : Category ℓ ℓ'}
         → Bifunctor C D E
         → Functor _×C_ E
-  rec {E = E} G = Presented.rec Q Ax E ı λ
+  rec {E = E} G = ProdCat.rec E (Free.rec Q ı) λ
       { (×-id c d) → G .Bif-×-id
       ; (×-seq f f' g g') → G .Bif-×-seq f f' g g'
       ; (L×-agree f d) → G .Bif-L×-agree f
       ; (R×-agree c g) → G .Bif-R×-agree g } where
       ı : Interp Q E
-      ı .I-ob (c , d) = G ⟅ c , d ⟆b
-      ı .I-hom (homR c g) = G ⟪ g ⟫r
-      ı .I-hom (homL f d) = G ⟪ f ⟫l
-      ı .I-hom (hom× f g) = G ⟪ f , g ⟫×
+      ı $g (c , d) = G ⟅ c , d ⟆b
+      ı <$g> homR c g = G ⟪ g ⟫r
+      ı <$g> homL f d = G ⟪ f ⟫l
+      ı <$g> hom× f g = G ⟪ f , g ⟫×
 
   ProdToRedundant : Functor (C BP.×C D) _×C_
   ProdToRedundant .F-ob (c , d) = c , d

Cubical/Categories/Constructions/Free/Category/Quiver.agda

@@ -10,13 +10,16 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.HLevels
 
 open import Cubical.Data.Sigma
+open import Cubical.Data.Quiver.Base as Quiver
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Base.More
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.UnderlyingGraph hiding (Interp)
 
-open import Cubical.Categories.Displayed.Section
+open import Cubical.Categories.Displayed.Section as Cat
 open import Cubical.Categories.Displayed.Preorder as Preorder hiding (Section)
 
 private
@@ -25,22 +28,7 @@ private
 
 open Category
 open Functor
-
-record QuiverOver (ob : Type ℓg) ℓg' : Type (ℓ-suc (ℓ-max ℓg ℓg')) where
-  field
-    mor : Type ℓg'
-    dom : mor → ob
-    cod : mor → ob
-
 open QuiverOver
-Quiver : ∀ ℓg ℓg' → Type _
-Quiver ℓg ℓg' = Σ[ ob ∈ Type ℓg ] QuiverOver ob ℓg'
-
-CatQuiver : Category ℓc ℓc' → Quiver ℓc (ℓ-max ℓc ℓc')
-CatQuiver 𝓒 .fst = 𝓒 .ob
-CatQuiver 𝓒 .snd .mor = Σ[ A ∈ 𝓒 .ob ] Σ[ B ∈ 𝓒 .ob ] (𝓒 [ A , B ])
-CatQuiver 𝓒 .snd .dom x = x .fst
-CatQuiver 𝓒 .snd .cod x = x .snd .fst
 
 module _ (Q : Quiver ℓg ℓg') where
   data Exp : Q .fst → Q .fst → Type (ℓ-max ℓg ℓg') where
@@ -63,31 +51,32 @@ module _ (Q : Quiver ℓg ℓg') where
   FreeCat .⋆Assoc = ⋆ₑAssoc
   FreeCat .isSetHom = isSetExp
 
-  -- A displayed interpretation
-  open Categoryᴰ
-  record Interpᴰ (𝓓 : Categoryᴰ FreeCat ℓd ℓd')
-    : Type ((ℓ-max (ℓ-max ℓg ℓg') (ℓ-max ℓd ℓd'))) where
-    field
-      I-ob : (c : Q .fst) → ob[_] 𝓓 c
-      I-hom : ∀ e → 𝓓 [ ↑ e ][ I-ob (Q .snd .dom e) , I-ob (Q .snd .cod e) ]
-  open Interpᴰ
+  Interp : (𝓒 : Category ℓc ℓc') → Type (ℓ-max (ℓ-max (ℓ-max ℓg ℓg') ℓc) ℓc')
+  Interp 𝓒 = HetQG Q (Cat→Graph 𝓒)
 
-  module _ {𝓓 : Categoryᴰ FreeCat ℓd ℓd'} (ı : Interpᴰ 𝓓) where
-    open Section
+  η : Interp FreeCat
+  η HetQG.$g x = x
+  η HetQG.<$g> e = ↑ e
 
+  module _ (𝓓 : Categoryᴰ FreeCat ℓd ℓd') where
+    Interpᴰ : Type _
+    Interpᴰ = Quiver.Section (Quiver.reindex η (Categoryᴰ→Graphᴰ 𝓓))
+
+  module _ {𝓓 : Categoryᴰ FreeCat ℓd ℓd'} (ı : Interpᴰ 𝓓) where
     private
+      module ı = Quiver.Section ı
       module 𝓓 = Categoryᴰ 𝓓
 
     elimF : ∀ {c c'} (f : FreeCat [ c , c' ])
-          → 𝓓 [ f ][ ı .I-ob c , ı .I-ob c' ]
-    elimF (↑ e) = ı .I-hom e
-    elimF idₑ = 𝓓 .idᴰ
+          → 𝓓 [ f ][ ı.F-ob c , ı.F-ob c' ]
+    elimF (↑ e) = ı.F-hom e
+    elimF idₑ = 𝓓.idᴰ
     elimF (f ⋆ₑ g) = elimF f 𝓓.⋆ᴰ elimF g
-    elimF (⋆ₑIdL f i) = 𝓓 .⋆IdLᴰ (elimF f) i
-    elimF (⋆ₑIdR f i) = 𝓓 .⋆IdRᴰ (elimF f) i
-    elimF (⋆ₑAssoc f f₁ f₂ i) = 𝓓 .⋆Assocᴰ (elimF f) (elimF f₁) (elimF f₂) i
+    elimF (⋆ₑIdL f i) = 𝓓.⋆IdLᴰ (elimF f) i
+    elimF (⋆ₑIdR f i) = 𝓓.⋆IdRᴰ (elimF f) i
+    elimF (⋆ₑAssoc f f₁ f₂ i) = 𝓓.⋆Assocᴰ (elimF f) (elimF f₁) (elimF f₂) i
     elimF (isSetExp f g p q i j) =
-      isOfHLevel→isOfHLevelDep 2 (λ x → 𝓓 .isSetHomᴰ)
+      isOfHLevel→isOfHLevelDep 2 (λ x → 𝓓.isSetHomᴰ)
       (elimF f)
       (elimF g)
       (cong elimF p)
@@ -96,22 +85,30 @@ module _ (Q : Quiver ℓg ℓg') where
       i
       j
 
-    elim : Section 𝓓
-    elim .F-ob = ı .I-ob
+    open Cat.Section
+    elim : Cat.Section 𝓓
+    elim .F-ob = ı.F-ob
     elim .F-hom = elimF
     elim .F-id = refl
     elim .F-seq f g = refl
 
-  -- Trivially displayed version of Interpᴰ
-  Interp : (𝓒 : Category ℓc ℓc') → Type (ℓ-max (ℓ-max (ℓ-max ℓg ℓg') ℓc) ℓc')
-  Interp 𝓒 = Interpᴰ (weaken FreeCat 𝓒)
+  module _ {ℓc ℓc'} {𝓒 : Categoryᴰ FreeCat ℓc ℓc'} (F G : Cat.Section 𝓒)
+    (agree-on-gen : Interpᴰ (Preorderᴰ→Catᴰ (SecPath _ F G))) where
+    FreeCatSection≡ : F ≡ G
+    FreeCatSection≡ =
+      SecPathSectionToSectionPath
+        _
+        (Iso.inv (PreorderSectionIsoCatSection _ _) (elim agree-on-gen))
 
-  η : Interp FreeCat
-  η .I-ob = λ c → c
-  η .I-hom = ↑_
+  module _ {𝓒 : Category ℓc ℓc'} (ı : Interp 𝓒) where
+    private
+      open HetQG
+      ıᴰ : Interpᴰ (weaken FreeCat 𝓒)
+      ıᴰ .Section.F-ob q  = ı $g q
+      ıᴰ .Section.F-hom e = ı <$g> e
 
-  rec : {𝓒 : Category ℓc ℓc'} → Interp 𝓒 → Functor FreeCat 𝓒
-  rec ı = Iso.fun (SectionToWkIsoFunctor _ _) (elim ı)
+    rec : Functor FreeCat 𝓒
+    rec = Iso.fun (SectionToWkIsoFunctor _ _) (elim ıᴰ)
 
   module _ {ℓc ℓc'} {𝓒 : Category ℓc ℓc'} (F G : Functor FreeCat 𝓒)
            (agree-on-gen :
@@ -121,7 +118,6 @@ module _ (Q : Quiver ℓg ℓg') where
                      (Iso.inv (SectionToWkIsoFunctor _ _) G))))
          where
     FreeCatFunctor≡ : F ≡ G
-    FreeCatFunctor≡ = isoInvInjective (SectionToWkIsoFunctor _ _) F G
-      (SecPathSectionToSectionPath (weaken FreeCat 𝓒)
-      (Iso.inv (PreorderSectionIsoCatSection _ _)
-      (elim agree-on-gen)))
+    FreeCatFunctor≡ =
+      isoInvInjective (SectionToWkIsoFunctor _ _) F G
+                      (FreeCatSection≡ _ _ agree-on-gen)