Representable Presheaves, Free Category, Functor and Associated solve…

…rs (#988)

* Define representability, universal morphisms, and their isomorphism

* a more universe polymorphic version of Yoneda

* application and λ for functor categories

* up universe polymorphism in representation/universal element

* a record formulation of universal elements

* Define a morphism of presheaves, and when a morphism preserves repr

* refactor to simplify proofs/better typechecking perf

* Rename universe polymorphic yoneda, add definition of PshIso, comments

* fix whitespace

* Free Category and Category Solver

* Free Functor and Functor Solver

* fix whitespace, document category solver better

* change uniqueness of free categories, fix column overflows

* Fix more column overflows

* Rename some things, add summary comments, remove vague comments

* fix build error, use camelCase

* order imports by category

* add BSD 3 license to the file adapted from 1lab

* update Free.Functor to work with Data.Equality, comment why Data.Equality is used

* rename UnivElt to UniversalElement, redefine in terms of isEquiv

Cubical/Categories/Constructions/Elements.agda

@@ -21,14 +21,16 @@ open Category
 open Functor
 
 module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
-
     getIsSet : ∀ {ℓS} {C : Category ℓ ℓ'} (F : Functor C (SET ℓS)) → (c : C .ob) → isSet (fst (F ⟅ c ⟆))
     getIsSet F c = snd (F ⟅ c ⟆)
 
+    Element : ∀ {ℓS} (F : Functor C (SET ℓS)) → Type (ℓ-max ℓ ℓS)
+    Element F = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
+
     infix 50 ∫_
     ∫_ : ∀ {ℓS} → Functor C (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
     -- objects are (c , x) pairs where c ∈ C and x ∈ F c
-    (∫ F) .ob = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
+    (∫ F) .ob = Element F
     -- morphisms are f : c → c' which take x to x'
     (∫ F) .Hom[_,_] (c , x) (c' , x')  = Σ[ f ∈ C [ c , c' ] ] x' ≡ (F ⟪ f ⟫) x
     (∫ F) .id {x = (c , x)} = C .id , sym (funExt⁻ (F .F-id) x ∙ refl)
@@ -85,6 +87,9 @@ module Contravariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
     ∫ᴾ_ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
     ∫ᴾ F = (∫ F) ^op
 
+    Elementᴾ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Type (ℓ-max ℓ ℓS)
+    Elementᴾ F = (∫ᴾ F) .ob
+
     -- helpful results
 
     module _ {ℓS} {F : Functor (C ^op) (SET ℓS)} where
@@ -95,3 +100,7 @@ module Contravariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
               → (eqInC : PathP (λ i → C [ fst (p i) , fst (q i) ]) (fst f) (fst g))
               → PathP (λ i → (∫ᴾ F) [ p i , q i ]) f g
       ∫ᴾhomEq _ _ _ _ = ΣPathPProp (λ f → snd (F ⟅ _ ⟆) _ _)
+
+      ∫ᴾhomEqSimpl : ∀ {o1 o2} (f g : (∫ᴾ F) [ o1 , o2 ])
+                   → fst f ≡ fst g → f ≡ g
+      ∫ᴾhomEqSimpl f g p = ∫ᴾhomEq f g refl refl p

Cubical/Categories/Constructions/Free/Category.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Constructions.Free.Category where
+
+open import Cubical.Categories.Constructions.Free.Category.Base public

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

@@ -0,0 +1,168 @@
+-- Free category over a directed graph, along with (most of) its
+-- universal property.
+
+-- This differs from the implementation in Free.Category, which
+-- assumes the vertices of the input graph form a Set.
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Constructions.Free.Category.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Path
+
+open import Cubical.Data.Graph.Base
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Morphism
+open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧)
+open import Cubical.Categories.UnderlyingGraph
+
+private
+  variable
+    ℓc ℓc' ℓd ℓd' ℓg ℓg' : Level
+
+open Category
+open Functor
+open NatIso hiding (sqRL; sqLL)
+open NatTrans
+
+module FreeCategory (G : Graph ℓg ℓg') where
+    data Exp : G .Node → G .Node → Type (ℓ-max ℓg ℓg') where
+      ↑_   : ∀ {A B} → G .Edge A B → Exp A B
+      idₑ  : ∀ {A} → Exp A A
+      _⋆ₑ_ : ∀ {A B C} → Exp A B → Exp B C → Exp A C
+      ⋆ₑIdL : ∀ {A B} (e : Exp A B) → idₑ ⋆ₑ e ≡ e
+      ⋆ₑIdR : ∀ {A B} (e : Exp A B) → e ⋆ₑ idₑ ≡ e
+      ⋆ₑAssoc : ∀ {A B C D} (e : Exp A B)(f : Exp B C)(g : Exp C D)
+              → (e ⋆ₑ f) ⋆ₑ g ≡ e ⋆ₑ (f ⋆ₑ g)
+      isSetExp : ∀ {A B} → isSet (Exp A B)
+
+    FreeCat : Category ℓg (ℓ-max ℓg ℓg')
+    FreeCat .ob = G .Node
+    FreeCat .Hom[_,_] = Exp
+    FreeCat .id = idₑ
+    FreeCat ._⋆_ = _⋆ₑ_
+    FreeCat .⋆IdL = ⋆ₑIdL
+    FreeCat .⋆IdR = ⋆ₑIdR
+    FreeCat .⋆Assoc = ⋆ₑAssoc
+    FreeCat .isSetHom = isSetExp
+
+    η : Interp G FreeCat
+    η ._$g_ = λ z → z
+    η ._<$g>_ = ↑_
+
+    module _ {ℓc ℓc'} {𝓒 : Category ℓc ℓc'} (F F' : Functor FreeCat 𝓒) where
+      -- Formulating uniqueness this way works out best definitionally.
+
+      -- If you prove induction from the alternative below of
+      --   sem-uniq : (F ∘Interp η ≡ ı) → F ≡ sem ı
+      -- then you have to use path comp which has bad definitional behavior
+      module _  (agree-on-η : F ∘Interp η ≡ F' ∘Interp η) where
+        private
+          aoo : ∀ c → F ⟅ c ⟆ ≡ F' ⟅ c ⟆
+          aoo = (λ c i → agree-on-η i $g c)
+
+          aom-t : ∀ {c c'} (e : Exp c c') → Type _
+          aom-t {c}{c'} e =
+            PathP (λ i → 𝓒 [ aoo c i , aoo c' i ]) (F ⟪ e ⟫) (F' ⟪ e ⟫)
+
+          aom-id : ∀ {c} → aom-t (idₑ {c})
+          aom-id = F .F-id ◁ (λ i → 𝓒 .id) ▷ sym (F' .F-id)
+
+          aom-seq : ∀ {c c' c''} (e : Exp c c')(e' : Exp c' c'')
+                  → aom-t e → aom-t e' → aom-t (e ⋆ₑ e')
+          aom-seq e e' ihe ihe' =
+            F .F-seq e e' ◁ (λ i → ihe i ⋆⟨ 𝓒 ⟩ ihe' i) ▷ sym (F' .F-seq e e')
+
+          aom : ∀ {c c'} (e : Exp c c') → aom-t e
+          aom (↑ x) = λ i → agree-on-η i <$g> x
+          aom idₑ = aom-id
+          aom (e ⋆ₑ e') = aom-seq e e' (aom e) (aom e')
+          aom (⋆ₑIdL e i) =
+            isSet→SquareP
+              (λ i j → 𝓒 .isSetHom)
+              (aom-seq idₑ e aom-id (aom e))
+              (aom e)
+              (λ i → F ⟪ ⋆ₑIdL e i ⟫) ((λ i → F' ⟪ ⋆ₑIdL e i ⟫)) i
+          aom (⋆ₑIdR e i) =
+            isSet→SquareP
+            (λ i j → 𝓒 .isSetHom)
+            (aom-seq e idₑ (aom e) aom-id)
+            (aom e)
+            (λ i → F ⟪ ⋆ₑIdR e i ⟫) ((λ i → F' ⟪ ⋆ₑIdR e i ⟫)) i
+          aom (⋆ₑAssoc e e' e'' i) =
+            isSet→SquareP
+            (λ _ _ → 𝓒 .isSetHom)
+            (aom-seq _ _ (aom-seq _ _ (aom e) (aom e')) (aom e''))
+            (aom-seq _ _ (aom e) (aom-seq _ _ (aom e') (aom e'')))
+            ((λ i → F ⟪ ⋆ₑAssoc e e' e'' i ⟫))
+            (λ i → F' ⟪ ⋆ₑAssoc e e' e'' i ⟫)
+            i
+          aom (isSetExp e e' x y i j) =
+            isSet→SquareP
+            {A = λ i j → aom-t (isSetExp e e' x y i j)}
+            (λ i j → isOfHLevelPathP 2 (𝓒 .isSetHom)
+                       (F ⟪ isSetExp e e' x y i j ⟫)
+                       (F' ⟪ isSetExp e e' x y i j ⟫))
+            (λ j → aom (x j))
+            (λ j → aom (y j))
+            (λ i → aom e)
+            (λ i → aom e')
+            i
+            j
+        induction : F ≡ F'
+        induction = Functor≡ aoo aom
+
+    module Semantics {ℓc ℓc'}
+                     (𝓒 : Category ℓc ℓc')
+                     (ı : GraphHom G (Cat→Graph 𝓒)) where
+      ⟦_⟧ : ∀ {A B} → Exp A B → 𝓒 [ ı $g A , ı $g B ]
+      ⟦ ↑ x ⟧ = ı <$g> x
+      ⟦ idₑ ⟧ = 𝓒 .id
+      ⟦ e ⋆ₑ e' ⟧ = ⟦ e ⟧ ⋆⟨ 𝓒 ⟩ ⟦ e' ⟧
+      ⟦ ⋆ₑIdL e i ⟧ = 𝓒 .⋆IdL ⟦ e ⟧ i
+      ⟦ ⋆ₑIdR e i ⟧ = 𝓒 .⋆IdR ⟦ e ⟧ i
+      ⟦ ⋆ₑAssoc e e' e'' i ⟧ = 𝓒 .⋆Assoc ⟦ e ⟧ ⟦ e' ⟧ ⟦ e'' ⟧ i
+      ⟦ isSetExp e e' p q i j ⟧ =
+        𝓒 .isSetHom ⟦ e ⟧ ⟦ e' ⟧ (cong ⟦_⟧ p) (cong ⟦_⟧ q) i j
+
+      sem : Functor FreeCat 𝓒
+      sem .Functor.F-ob v = ı $g v
+      sem .Functor.F-hom e = ⟦ e ⟧
+      sem .Functor.F-id = refl
+      sem .Functor.F-seq e e' = refl
+
+      sem-extends-ı : (η ⋆Interp sem) ≡ ı
+      sem-extends-ı = refl
+
+      sem-uniq : ∀ {F : Functor FreeCat 𝓒} → ((Functor→GraphHom F ∘GrHom η) ≡ ı) → F ≡ sem
+      sem-uniq {F} aog = induction F sem aog
+
+      sem-contr : ∃![ F ∈ Functor FreeCat 𝓒 ] Functor→GraphHom F ∘GrHom η ≡ ı
+      sem-contr .fst = sem , sem-extends-ı
+      sem-contr .snd (sem' , sem'-extends-ı) = ΣPathP paths
+        where
+          paths : Σ[ p ∈ sem ≡ sem' ]
+                  PathP (λ i → Functor→GraphHom (p i) ∘GrHom η ≡ ı)
+                        sem-extends-ı
+                        sem'-extends-ı
+          paths .fst = sym (sem-uniq sem'-extends-ı)
+          paths .snd i j = sem'-extends-ı ((~ i) ∨ j)
+
+    η-expansion : {𝓒 : Category ℓc ℓc'} (F : Functor FreeCat 𝓒)
+      → F ≡ Semantics.sem 𝓒 (F ∘Interp η)
+    η-expansion {𝓒 = 𝓒} F = induction F (Semantics.sem 𝓒 (F ∘Interp η)) refl
+
+-- co-unit of the 2-adjunction
+module _ {𝓒 : Category ℓc ℓc'} where
+  open FreeCategory (Cat→Graph 𝓒)
+  ε : Functor FreeCat 𝓒
+  ε = Semantics.sem 𝓒 (Functor→GraphHom {𝓓 = 𝓒} Id)
+
+  ε-reasoning : {𝓓 : Category ℓd ℓd'}
+            → (𝓕 : Functor 𝓒 𝓓)
+            → 𝓕 ∘F ε ≡ Semantics.sem 𝓓 (Functor→GraphHom 𝓕)
+  ε-reasoning {𝓓 = 𝓓} 𝓕 = Semantics.sem-uniq 𝓓 (Functor→GraphHom 𝓕) refl