Construct 'the' free wild category on a graph

Cubical/Categories/Constructions/Free.agda

@@ -19,8 +19,8 @@ module _ {ℓv ℓe : Level} where
     FreeCategory .ob = Node G
     FreeCategory .Hom[_,_] = Path G
     FreeCategory .id = pnil
-    FreeCategory ._⋆_ = ccat G
-    FreeCategory .⋆IdL = pnil++ G
-    FreeCategory .⋆IdR P = refl
-    FreeCategory .⋆Assoc = ++assoc G
-    FreeCategory .isSetHom = isSetPath G isSetNode isSetEdge _ _
+    FreeCategory ._⋆_ = _++_
+    FreeCategory .⋆IdL = pnil++
+    FreeCategory .⋆IdR P = ++pnil _
+    FreeCategory .⋆Assoc = ++assoc
+    FreeCategory .isSetHom = isSetPath isSetNode isSetEdge _ _

Cubical/Data/Graph/Path.agda

@@ -3,79 +3,99 @@
 
 module Cubical.Data.Graph.Path where
 
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Prelude hiding (Path)
+
 open import Cubical.Data.Graph.Base
-open import Cubical.Data.List.Base hiding (_++_)
+open import Cubical.Data.List.Base hiding (_++_; map)
 open import Cubical.Data.Nat.Base
 open import Cubical.Data.Nat.Properties
 open import Cubical.Data.Sigma.Base hiding (Path)
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Prelude hiding (Path)
-
 
-module _ {ℓv ℓe : Level} where
-
-  module _ (G : Graph ℓv ℓe) where
-    data Path : (v w : Node G) → Type (ℓ-max ℓv ℓe) where
-      pnil : ∀ {v} → Path v v
-      pcons : ∀ {v w x} → Path v w → Edge G w x → Path v x
-
-    -- Path concatenation
-    ccat : ∀ {v w x} → Path v w → Path w x → Path v x
-    ccat P pnil = P
-    ccat P (pcons Q e) = pcons (ccat P Q) e
-
-    private
-      _++_ = ccat
-      infixr 20 _++_
-
-    -- Some properties
-    pnil++ : ∀ {v w} (P : Path v w) → pnil ++ P ≡ P
-    pnil++ pnil = refl
-    pnil++ (pcons P e) = cong (λ P → pcons P e) (pnil++ _)
-
-    ++assoc : ∀ {v w x y}
-        (P : Path v w) (Q : Path w x) (R : Path x y)
-      → (P ++ Q) ++ R ≡ P ++ (Q ++ R)
-    ++assoc P Q pnil = refl
-    ++assoc P Q (pcons R e) = cong (λ P → pcons P e) (++assoc P Q R)
-
-    -- Paths as lists
-    pathToList : ∀ {v w} → Path v w
-        → List (Σ[ x ∈ Node G ] Σ[ y ∈ Node G ] Edge G x y)
-    pathToList pnil = []
-    pathToList (pcons P e) = (_ , _ , e) ∷ (pathToList P)
-
-    -- Path v w is a set
-    -- Lemma 4.2 of https://arxiv.org/abs/2112.06609
-    module _ (isSetNode : isSet (Node G))
-             (isSetEdge : ∀ v w → isSet (Edge G v w)) where
-
-      -- This is called ̂W (W-hat) in the paper
-      PathWithLen : ℕ → Node G → Node G → Type (ℓ-max ℓv ℓe)
-      PathWithLen 0 v w = Lift {j = ℓe} (v ≡ w)
-      PathWithLen (suc n) v w = Σ[ k ∈ Node G ] (PathWithLen n v k × Edge G k w)
-
-      isSetPathWithLen : ∀ n v w → isSet (PathWithLen n v w)
-      isSetPathWithLen 0 _ _ = isOfHLevelLift 2 (isProp→isSet (isSetNode _ _))
-      isSetPathWithLen (suc n) _ _ = isSetΣ isSetNode λ _ →
-          isSet× (isSetPathWithLen _ _ _) (isSetEdge _ _)
-
-      isSet-ΣnPathWithLen : ∀ {v w} → isSet (Σ[ n ∈ ℕ ] PathWithLen n v w)
-      isSet-ΣnPathWithLen = isSetΣ isSetℕ (λ _ → isSetPathWithLen _ _ _)
-
-      Path→PathWithLen : ∀ {v w} → Path v w → Σ[ n ∈ ℕ ] PathWithLen n v w
-      Path→PathWithLen pnil = 0 , lift refl
-      Path→PathWithLen (pcons P e) = suc (Path→PathWithLen P .fst) ,
-                                          _ , Path→PathWithLen P .snd , e
-
-      PathWithLen→Path : ∀ {v w} → Σ[ n ∈ ℕ ] PathWithLen n v w → Path v w
-      PathWithLen→Path (0 , q) = subst (Path _) (q .lower) pnil
-      PathWithLen→Path (suc n , _ , pwl , e) = pcons (PathWithLen→Path (n , pwl)) e
-
-      Path→PWL→Path : ∀ {v w} P → PathWithLen→Path {v} {w} (Path→PathWithLen P) ≡ P
-      Path→PWL→Path {v} pnil = substRefl {B = Path v} pnil
-      Path→PWL→Path (pcons P x) = cong₂ pcons (Path→PWL→Path _) refl
-
-      isSetPath : ∀ v w → isSet (Path v w)
-      isSetPath v w = isSetRetract Path→PathWithLen PathWithLen→Path
-                                   Path→PWL→Path isSet-ΣnPathWithLen
+private variable
+  ℓv ℓe ℓv' ℓe'  : Level
+
+module _ (G : Graph ℓv ℓe) where
+  data Path : (v w : Node G) → Type (ℓ-max ℓv ℓe) where
+    pnil : ∀ {v} → Path v v
+    pcons : ∀ {v x w} → Edge G v x → Path x w → Path v w
+
+module _ {G : Graph ℓv ℓe} where
+
+  -- Path concatenation
+  ccat : ∀ {v x w} → Path G v x → Path G x w → Path G v w
+  ccat pnil Q = Q
+  ccat (pcons e P) Q = pcons e (ccat P Q)
+
+  _++_ = ccat
+  infixr 20 _++_
+
+  -- Some properties
+  pnil++ : ∀ {v w} (P : Path G v w) → pnil ++ P ≡ P
+  pnil++ pnil = refl
+  pnil++ (pcons e P) = cong (λ P → pcons e P) (pnil++ _)
+
+  ++pnil : ∀ {v w} (P : Path G v w) → P ++ pnil ≡ P
+  ++pnil pnil = refl
+  ++pnil (pcons e P) = cong (λ P → pcons e P) (++pnil P)
+
+  ++assoc : ∀ {v w x y}
+      (P : Path G v w) (Q : Path G w x) (R : Path G x y)
+    → (P ++ Q) ++ R ≡ P ++ (Q ++ R)
+  ++assoc pnil P Q = refl
+  ++assoc (pcons e P) Q R = cong (λ P → pcons e P) (++assoc P Q R)
+
+  -- Paths as lists
+  pathToList : ∀ {v w} → Path G v w
+      → List (Σ[ x ∈ Node G ] Σ[ y ∈ Node G ] Edge G x y)
+  pathToList pnil = []
+  pathToList (pcons e P) = (_ , _ , e) ∷ (pathToList P)
+
+  -- Path v w is a set
+  -- Lemma 4.2 of https://arxiv.org/abs/2112.06609
+  module _ (isSetNode : isSet (Node G))
+           (isSetEdge : ∀ v w → isSet (Edge G v w)) where
+
+    -- This is called ̂W (W-hat) in the paper
+    PathWithLen : ℕ → Node G → Node G → Type (ℓ-max ℓv ℓe)
+    PathWithLen 0 v w = Lift {j = ℓe} (v ≡ w)
+    PathWithLen (suc n) v w = Σ[ x ∈ Node G ] (Edge G v x × PathWithLen n x w)
+
+    isSetPathWithLen : ∀ n v w → isSet (PathWithLen n v w)
+    isSetPathWithLen 0 _ _ = isOfHLevelLift 2 (isProp→isSet (isSetNode _ _))
+    isSetPathWithLen (suc n) _ _ = isSetΣ isSetNode λ _ →
+        isSet× (isSetEdge _ _) (isSetPathWithLen _ _ _)
+
+    isSet-ΣnPathWithLen : ∀ {v w} → isSet (Σ[ n ∈ ℕ ] PathWithLen n v w)
+    isSet-ΣnPathWithLen = isSetΣ isSetℕ (λ _ → isSetPathWithLen _ _ _)
+
+    Path→PathWithLen : ∀ {v w} → Path G v w → Σ[ n ∈ ℕ ] PathWithLen n v w
+    Path→PathWithLen pnil = 0 , lift refl
+    Path→PathWithLen (pcons e P) = suc (Path→PathWithLen P .fst) , _ , e , Path→PathWithLen P .snd
+
+    PathWithLen→Path : ∀ {v w} → Σ[ n ∈ ℕ ] PathWithLen n v w → Path G v w
+    PathWithLen→Path (0 , q) = subst (Path G _) (q .lower) pnil
+    PathWithLen→Path (suc n , _ , e , pwl) = pcons e (PathWithLen→Path (n , pwl))
+
+    Path→PWL→Path : ∀ {v w} P → PathWithLen→Path {v} {w} (Path→PathWithLen P) ≡ P
+    Path→PWL→Path {v} pnil = substRefl {B = Path G v} pnil
+    Path→PWL→Path (pcons P x) = cong₂ pcons refl (Path→PWL→Path _)
+
+    isSetPath : ∀ v w → isSet (Path G v w)
+    isSetPath v w = isSetRetract Path→PathWithLen PathWithLen→Path
+                                 Path→PWL→Path isSet-ΣnPathWithLen
+
+module _ {G : Graph ℓv ℓe} {H : Graph ℓv' ℓe'} where
+  open GraphHom
+  map : {x y : Node G}
+        (F : GraphHom G H)
+        → Path G x y → Path H (F $g x) (F $g y)
+  map F pnil = pnil
+  map F (pcons e p) = pcons (F <$g> e) (map F p)
+
+  map++ : {x y z : Node G}
+        (F : GraphHom G H)
+        → (p : Path G x y) → (q : Path G y z)
+        → map F (p ++ q) ≡ map F p ++ map F q
+  map++ F pnil q = refl
+  map++ F (pcons x p) q = cong (λ m → pcons (F <$g> x) m) (map++ F p q)

Cubical/WildCat/Base.agda

@@ -38,11 +38,11 @@ _[_,_] : (C : WildCat ℓ ℓ') → (x y : C .ob) → Type ℓ'
 _[_,_] = Hom[_,_]
 
 -- Needed to define this in order to be able to make the subsequence syntax declaration
-seq' : ∀ (C : WildCat ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
-seq' = _⋆_
+concatMor : ∀ (C : WildCat ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
+concatMor = _⋆_
 
-infixl 15 seq'
-syntax seq' C f g = f ⋆⟨ C ⟩ g
+infixl 15 concatMor
+syntax concatMor C f g = f ⋆⟨ C ⟩ g
 
 -- composition
 comp' : ∀ (C : WildCat ℓ ℓ') {x y z} (g : C [ y , z ]) (f : C [ x , y ]) → C [ x , z ]

Cubical/WildCat/Free.agda

@@ -0,0 +1,74 @@
+{-
+  This file defines a wild category, which might be the free wild category over a
+  directed graph (I do not know). This is intended to be used in a solver for
+  wild categories.
+-}
+{-# OPTIONS --safe #-}
+
+module Cubical.WildCat.Free where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Graph.Base
+open import Cubical.Data.Graph.Path renaming (Path to GPath)
+
+open import Cubical.WildCat.Base
+open import Cubical.WildCat.Functor
+open import Cubical.WildCat.UnderlyingGraph
+
+open WildCat
+open WildFunctor
+open Graph
+
+private
+  variable
+    ℓc ℓc' ℓd ℓd' ℓg ℓg' : Level
+
+Free : (G : Graph ℓg ℓg') → WildCat ℓg (ℓ-max ℓg ℓg')
+ob (Free G) = G .Node
+Hom[_,_] (Free G) x y = GPath G x y
+id (Free G) = pnil
+_⋆_ (Free G) f g = f ++ g
+⋆IdL (Free G) = λ _ → refl
+⋆IdR (Free G) = ++pnil
+⋆Assoc (Free G) f g h = ++assoc f g h
+
+composeAll : (C : WildCat ℓc ℓc') {x y : ob C} → GPath (Cat→Graph C) x y → C [ x , y ]
+composeAll C pnil = id C
+composeAll C (pcons m path) = m ⋆⟨ C ⟩ composeAll C path
+
+
+composeAll++ : (C : WildCat ℓc ℓc') {x y z : ob C}
+               → (p : GPath (Cat→Graph C) x y) → (q : GPath (Cat→Graph C) y z)
+               → composeAll C (p ++ q) ≡ composeAll C p ⋆⟨ C ⟩ composeAll C q
+composeAll++ C pnil q = sym (⋆IdL C (composeAll C q))
+composeAll++ C (pcons m p) q =
+  composeAll C (pcons m p ++ q)                       ≡⟨ step1 ⟩
+  m ⋆⟨ C ⟩ ((composeAll C p) ⋆⟨ C ⟩ (composeAll C q)) ≡⟨ sym (⋆Assoc C m (composeAll C p) (composeAll C q)) ⟩
+  (m ⋆⟨ C ⟩ (composeAll C p)) ⋆⟨ C ⟩ (composeAll C q) ∎
+  where step1 = cong (λ z → concatMor C m z) (composeAll++ C p q)
+
+module UniversalProperty (G : Graph ℓg ℓg') where
+
+
+  incFree : GraphHom G (Cat→Graph (Free G))
+  incFree $g x = x
+  incFree <$g> e = pcons e pnil
+
+  {-
+     G ──→ Free G
+      \    ∣
+   ∀ F \   ∣ ∃ F'
+        ↘  ↓
+          C
+  -}
+  inducedMorphism : (C : WildCat ℓc ℓc') → GraphHom G (Cat→Graph C) → WildFunctor (Free G) C
+  inducedMorphism C F = F'
+    where F' : WildFunctor (Free G) C
+          F-ob F' x = F $g x
+          F-hom F' m = composeAll C (map F m)
+          F-id F' = refl
+          F-seq F' f g =
+            composeAll C (map F (f ⋆⟨ Free G ⟩ g))                  ≡⟨ cong (λ u → composeAll C u) (map++ F f g) ⟩
+            composeAll C (map F f ++ map F g)                       ≡⟨ composeAll++ C (map F f) (map F g) ⟩
+            (composeAll C (map F f)) ⋆⟨ C ⟩ (composeAll C (map F g)) ∎

Cubical/WildCat/Functor.agda

@@ -162,3 +162,19 @@ WildFunctor.F-ob commFunctor (x , y) = y , x
 WildFunctor.F-hom commFunctor (f , g) = g , f
 WildFunctor.F-id commFunctor = refl
 WildFunctor.F-seq commFunctor _ _ = refl
+
+
+infixl 20 _$_
+_$_ : {ℓC ℓC' ℓD ℓD' : Level}
+      {C : WildCat ℓC ℓC'}
+      {D : WildCat ℓD ℓD'}
+   → WildFunctor C D → C .ob → D .ob
+F $ x = F .F-ob x
+
+infixl 20 _$→_
+_$→_ : {ℓC ℓC' ℓD ℓD' : Level}
+      {C : WildCat ℓC ℓC'}
+      {D : WildCat ℓD ℓD'}
+      {x y : C .ob}
+   → (F : WildFunctor C D) → C [ x , y ] → D [ F $ x , F $ y ]
+F $→ f = F .F-hom f

Cubical/WildCat/UnderlyingGraph.agda

@@ -0,0 +1,50 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.WildCat.UnderlyingGraph where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Graph.Base
+
+open import Cubical.WildCat.Base
+open import Cubical.WildCat.Functor
+
+private
+  variable
+    ℓc ℓc' ℓd ℓd' ℓe ℓe' ℓg ℓg' : Level
+
+open WildCat
+
+-- Underlying graph of a category
+Cat→Graph : ∀ {ℓc ℓc'} (𝓒 : WildCat ℓc ℓc') → Graph ℓc ℓc'
+Cat→Graph 𝓒 .Node = 𝓒 .ob
+Cat→Graph 𝓒 .Edge = 𝓒 .Hom[_,_]
+
+Functor→GraphHom : ∀ {ℓc ℓc' ℓd ℓd'} {𝓒 : WildCat ℓc ℓc'} {𝓓 : WildCat ℓd ℓd'}
+       (F : WildFunctor 𝓒 𝓓) → GraphHom (Cat→Graph 𝓒) (Cat→Graph 𝓓)
+Functor→GraphHom F ._$g_ = WildFunctor.F-ob F
+Functor→GraphHom F ._<$g>_ = WildFunctor.F-hom F
+
+
+module _ (G : Graph ℓg ℓg') (𝓒 : WildCat ℓc ℓc') where
+  -- Interpretation of a graph in a wild category
+  Interpret : Type _
+  Interpret = GraphHom G (Cat→Graph 𝓒)
+
+
+_⋆Interpret_ : ∀ {G : Graph ℓg ℓg'}
+              {𝓒 : WildCat ℓc ℓc'}
+              {𝓓 : WildCat ℓd ℓd'}
+              (ı : Interpret G 𝓒)
+              (F : WildFunctor 𝓒 𝓓)
+              → Interpret G 𝓓
+(ı ⋆Interpret F) ._$g_ x = WildFunctor.F-ob F (ı $g x)
+(ı ⋆Interpret F) ._<$g>_ e = WildFunctor.F-hom F (ı <$g> e)
+
+_∘Interpret_ : ∀ {G : Graph ℓg ℓg'}
+              {𝓒 : WildCat ℓc ℓc'}
+              {𝓓 : WildCat ℓd ℓd'}
+              (F : WildFunctor 𝓒 𝓓)
+              (ı : Interpret G 𝓒)
+              → Interpret G 𝓓
+F ∘Interpret ı = ı ⋆Interpret F