From 1a301f352f7b26dc72c399c5f8395d7c3d170e62 Mon Sep 17 00:00:00 2001 From: "Max S. New" Date: Mon, 10 Jul 2023 05:32:07 -0400 Subject: [PATCH] Representable Presheaves, Free Category, Functor and Associated solvers (#988) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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 --- .../Categories/Constructions/Elements.agda | 13 +- .../Constructions/Free/Category.agda | 5 + .../Constructions/Free/Category/Base.agda | 168 +++++++++ .../Constructions/Free/Functor.agda | 349 ++++++++++++++++++ Cubical/Categories/Constructions/Lift.agda | 37 ++ Cubical/Categories/Constructions/Power.agda | 27 ++ Cubical/Categories/Constructions/Product.agda | 39 +- Cubical/Categories/Instances/Functors.agda | 79 +++- Cubical/Categories/Instances/Sets.agda | 7 + Cubical/Categories/Limits/Terminal.agda | 28 +- .../NaturalTransformation/Properties.agda | 45 ++- Cubical/Categories/Presheaf.agda | 3 + Cubical/Categories/Presheaf/Base.agda | 29 +- Cubical/Categories/Presheaf/Morphism.agda | 96 +++++ Cubical/Categories/Presheaf/Properties.agda | 8 + .../Categories/Presheaf/Representable.agda | 196 ++++++++++ Cubical/Categories/UnderlyingGraph.agda | 56 +++ Cubical/Categories/Yoneda.agda | 105 +++++- Cubical/Data/Graph/Base.agda | 25 +- Cubical/Tactics/CategorySolver/Examples.agda | 46 +++ .../Tactics/CategorySolver/Reflection.agda | 61 +++ Cubical/Tactics/CategorySolver/Solver.agda | 57 +++ Cubical/Tactics/FunctorSolver/Examples.agda | 45 +++ Cubical/Tactics/FunctorSolver/Reflection.agda | 95 +++++ Cubical/Tactics/FunctorSolver/Solver.agda | 66 ++++ Cubical/Tactics/Reflection.agda | 114 ++++++ 26 files changed, 1763 insertions(+), 36 deletions(-) create mode 100644 Cubical/Categories/Constructions/Free/Category.agda create mode 100644 Cubical/Categories/Constructions/Free/Category/Base.agda create mode 100644 Cubical/Categories/Constructions/Free/Functor.agda create mode 100644 Cubical/Categories/Constructions/Lift.agda create mode 100644 Cubical/Categories/Constructions/Power.agda create mode 100644 Cubical/Categories/Presheaf/Morphism.agda create mode 100644 Cubical/Categories/Presheaf/Representable.agda create mode 100644 Cubical/Categories/UnderlyingGraph.agda create mode 100644 Cubical/Tactics/CategorySolver/Examples.agda create mode 100644 Cubical/Tactics/CategorySolver/Reflection.agda create mode 100644 Cubical/Tactics/CategorySolver/Solver.agda create mode 100644 Cubical/Tactics/FunctorSolver/Examples.agda create mode 100644 Cubical/Tactics/FunctorSolver/Reflection.agda create mode 100644 Cubical/Tactics/FunctorSolver/Solver.agda create mode 100644 Cubical/Tactics/Reflection.agda diff --git a/Cubical/Categories/Constructions/Elements.agda b/Cubical/Categories/Constructions/Elements.agda index 32ced627fe..5f28e6ccb9 100644 --- a/Cubical/Categories/Constructions/Elements.agda +++ b/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 diff --git a/Cubical/Categories/Constructions/Free/Category.agda b/Cubical/Categories/Constructions/Free/Category.agda new file mode 100644 index 0000000000..1b1cda7c79 --- /dev/null +++ b/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 diff --git a/Cubical/Categories/Constructions/Free/Category/Base.agda b/Cubical/Categories/Constructions/Free/Category/Base.agda new file mode 100644 index 0000000000..ccd734ce7e --- /dev/null +++ b/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 diff --git a/Cubical/Categories/Constructions/Free/Functor.agda b/Cubical/Categories/Constructions/Free/Functor.agda new file mode 100644 index 0000000000..79023cdb1e --- /dev/null +++ b/Cubical/Categories/Constructions/Free/Functor.agda @@ -0,0 +1,349 @@ +-- Free functor between categories generated from two graphs and a +-- function on nodes between them +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Categories.Constructions.Free.Functor where + +open import Cubical.Foundations.Prelude hiding (J) +open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Path +open import Cubical.Foundations.Transport + +open import Cubical.Data.Empty +open import Cubical.Data.Equality.Conversion +open import Cubical.Data.Equality hiding (id; sym) + renaming (_≡_ to Eq; refl to reflEq; _∙_ to _∙Eq_; transport to transportEq) +open import Cubical.Data.Graph.Base +open import Cubical.Data.Sigma + +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Constructions.Free.Category +open import Cubical.Categories.Functor.Base +open import Cubical.Categories.NaturalTransformation.Base +open import Cubical.Categories.UnderlyingGraph + +private + variable + ℓ ℓ' ℓc ℓc' ℓd ℓd' ℓg ℓg' ℓh ℓh' : Level + +open Category +open Functor +open NatTrans +open NatIso +open isIso + +module FreeFunctor (G : Graph ℓg ℓg') + (H : Graph ℓh ℓh') + (ϕ : G .Node → H .Node) where + module FreeCatG = FreeCategory G + open FreeCatG.Exp + FG = FreeCatG.FreeCat + Exp = FreeCatG.Exp + data FExp : H .Node → H .Node + → Type (((ℓ-max ℓg (ℓ-max ℓg' (ℓ-max ℓh ℓh'))))) where + -- free category on H with a functor from G to H freely added + ↑_ : ∀ {A B} → H .Edge A B → FExp A B + idₑ : ∀ {A} → FExp A A + _⋆ₑ_ : ∀ {A B C} → FExp A B → FExp B C → FExp A C + F⟪_⟫ : ∀ {A B} → Exp A B → FExp (ϕ A) (ϕ B) + + ⋆ₑIdL : ∀ {A B} (e : FExp A B) → idₑ ⋆ₑ e ≡ e + ⋆ₑIdR : ∀ {A B} (e : FExp A B) → e ⋆ₑ idₑ ≡ e + ⋆ₑAssoc : ∀ {A B C D} (e : FExp A B)(f : FExp B C)(g : FExp C D) + → (e ⋆ₑ f) ⋆ₑ g ≡ e ⋆ₑ (f ⋆ₑ g) + F-idₑ : ∀ {A} → F⟪ idₑ {A = A} ⟫ ≡ idₑ + F-seqₑ : ∀ {A B C} (f : Exp A B)(g : Exp B C) + → F⟪ f ⋆ₑ g ⟫ ≡ (F⟪ f ⟫ ⋆ₑ F⟪ g ⟫) + + isSetFExp : ∀ {A B} → isSet (FExp A B) + + FH : Category _ _ + FH .ob = H .Node + FH .Hom[_,_] = FExp + FH .id = idₑ + FH ._⋆_ = _⋆ₑ_ + FH .⋆IdL = ⋆ₑIdL + FH .⋆IdR = ⋆ₑIdR + FH .⋆Assoc = ⋆ₑAssoc + FH .isSetHom = isSetFExp + + Fϕ : Functor FG FH + Fϕ .F-ob = ϕ + Fϕ .F-hom = F⟪_⟫ + Fϕ .F-id = F-idₑ + Fϕ .F-seq = F-seqₑ + + -- The universal interpretation + ηG = FreeCatG.η + + ηH : Interp H FH + ηH $g x = x + ηH <$g> x = ↑ x + + Fϕ-homo : GraphHom G (Cat→Graph FH) + Fϕ-homo $g x = ϕ x + Fϕ-homo <$g> x = F⟪ ↑ x ⟫ + + ηϕ : Eq (Fϕ .F-ob ∘f ηG ._$g_) (ηH ._$g_ ∘f ϕ) + ηϕ = reflEq + + module _ {𝓒 : Category ℓc ℓc'}{𝓓 : Category ℓd ℓd'} {𝓕 : Functor 𝓒 𝓓} where + {- + + It is very important for the implementation of the functor + solver that ıϕ uses Data.Equality.Eq rather than Path. The + reason is that the case semH-hom (F⟪_⟫ {A}{B} x) inherently + involves a transport when expressed at this level of + generality, and transport of a refl is the identity function + for Eq but not for Path. + + -} + module Semantics (ıG : Interp G 𝓒) (ıH : Interp H 𝓓) + (ıϕ : Eq (𝓕 .F-ob ∘f ıG ._$g_) (ıH ._$g_ ∘f ϕ)) + where + semG = FreeCatG.Semantics.sem 𝓒 ıG + + semH-hom : ∀ {A B} → FExp A B → 𝓓 [ ıH $g A , ıH $g B ] + semH-hom (↑ x) = ıH <$g> x + semH-hom idₑ = 𝓓 .id + semH-hom (e ⋆ₑ e₁) = semH-hom e ⋆⟨ 𝓓 ⟩ semH-hom e₁ + semH-hom (F⟪_⟫ {A}{B} x) = + transportEq (λ (f : G .Node → 𝓓 .ob) → 𝓓 [ f A , f B ]) + ıϕ + (𝓕 ⟪ semG ⟪ x ⟫ ⟫) + semH-hom (⋆ₑIdL f i) = 𝓓 .⋆IdL (semH-hom f) i + semH-hom (⋆ₑIdR f i) = 𝓓 .⋆IdR (semH-hom f) i + semH-hom (⋆ₑAssoc f f' f'' i) = + 𝓓 .⋆Assoc (semH-hom f) (semH-hom f') (semH-hom f'') i + semH-hom (F-idₑ {A} i) = unbound i + where + unbound : transportEq (λ f → 𝓓 [ f A , f A ]) ıϕ (𝓕 ⟪ semG ⟪ idₑ ⟫ ⟫) + ≡ 𝓓 .id + unbound = + J (λ g p → transportEq (λ f → 𝓓 [ f A , f A ]) p + (𝓕 ⟪ semG ⟪ idₑ ⟫ ⟫) + ≡ 𝓓 .id) + ((𝓕 ∘F semG) .F-id) ıϕ + semH-hom (F-seqₑ {A}{B}{C} e e' i) = unbound i + where + unbound : + transportEq (λ f → 𝓓 [ f A , f C ]) ıϕ (𝓕 ⟪ semG ⟪ e ⋆ₑ e' ⟫ ⟫) + ≡ (transportEq (λ f → 𝓓 [ f A , f B ]) ıϕ (𝓕 ⟪ semG ⟪ e ⟫ ⟫)) + ⋆⟨ 𝓓 ⟩ (transportEq (λ f → 𝓓 [ f B , f C ]) ıϕ + (𝓕 ⟪ semG ⟪ e' ⟫ ⟫)) + unbound = + J (λ g p → + transportEq (λ f → 𝓓 [ f A , f C ]) p (𝓕 ⟪ semG ⟪ e ⋆ₑ e' ⟫ ⟫) + ≡ (transportEq (λ f → 𝓓 [ f A , f B ]) p (𝓕 ⟪ semG ⟪ e ⟫ ⟫)) + ⋆⟨ 𝓓 ⟩ (transportEq (λ f → 𝓓 [ f B , f C ]) p + (𝓕 ⟪ semG ⟪ e' ⟫ ⟫))) + ((𝓕 ∘F semG) .F-seq e e') + ıϕ + semH-hom (isSetFExp f g p q i j) = + 𝓓 .isSetHom (semH-hom f) + (semH-hom g) + (cong semH-hom p) + (cong semH-hom q) + i + j + + semH : Functor FH 𝓓 + semH .F-ob = ıH ._$g_ + semH .F-hom = semH-hom + semH .F-id = refl + semH .F-seq f g = refl + + semϕ : Eq (𝓕 ∘F semG) (semH ∘F Fϕ) + semϕ = pathToEq (FreeCatG.induction (funcComp 𝓕 semG) + (funcComp semH Fϕ) + (GrHom≡ aoo aoe)) + where + 𝓕G = (𝓕 .F-ob ∘f ıG ._$g_) + Hϕ = (ıH ._$g_ ∘f ϕ) + + aoo-gen : ∀ (v : Node G) f g + → Eq {A = G .Node → 𝓓 .ob} f g + → Path _ (f v) (g v) + aoo-gen v f g = J ((λ f' _ → Path _ (f v) (f' v))) refl + aoo : (v : Node G) + → Path _ (((𝓕 ∘F semG) ∘Interp ηG) $g v) + (((semH ∘F Fϕ) ∘Interp ηG) $g v) + aoo v = aoo-gen v 𝓕G Hϕ ıϕ + + aoe : {v w : Node G} (e : G .Edge v w) → + PathP (λ i → 𝓓 .Hom[_,_] (aoo v i) (aoo w i)) + (𝓕 ⟪ semG ⟪ ↑ e ⟫ ⟫) + (semH ⟪ Fϕ ⟪ ↑ e ⟫ ⟫) + aoe {v}{w} e = toPathP lem where + lem : Path _ + (transport (λ i → 𝓓 [ aoo-gen v 𝓕G Hϕ ıϕ i + , aoo-gen w 𝓕G Hϕ ıϕ i ]) + (𝓕 ⟪ ıG <$g> e ⟫)) + (transportEq (λ f → 𝓓 [ f v , f w ]) ıϕ (𝓕 ⟪ ıG <$g> e ⟫)) + lem = + J (λ f p → + Path _ + ((transport (λ i → 𝓓 [ aoo-gen v 𝓕G f p i + , aoo-gen w 𝓕G f p i ]) + (𝓕 ⟪ ıG <$g> e ⟫))) + ((transportEq (λ f → 𝓓 [ f v , f w ]) p + (𝓕 ⟪ ıG <$g> e ⟫)))) + (transportRefl (𝓕 ⟪ ıG <$g> e ⟫)) + ıϕ + + module Uniqueness (arb𝓒 : Functor FG 𝓒) + (arb𝓓 : Functor FH 𝓓) + (arb𝓕 : Path (Functor FG 𝓓) (𝓕 ∘F arb𝓒) (arb𝓓 ∘F Fϕ)) + (arb𝓒-agree : arb𝓒 ∘Interp ηG ≡ ıG) + (arb𝓓-agree : arb𝓓 ∘Interp ηH ≡ ıH) + (arb𝓕-agree : Square {A = G .Node → 𝓓 .ob} + (λ i x → arb𝓕 i ⟅ x ⟆) + (eqToPath ıϕ) + (λ i x → 𝓕 ⟅ arb𝓒-agree i $g x ⟆) + (λ i x → arb𝓓-agree i $g (ϕ x))) + where + sem-uniq-G : arb𝓒 ≡ semG + sem-uniq-G = FreeCatG.Semantics.sem-uniq _ _ arb𝓒-agree + + sem-uniq-H : arb𝓓 ≡ semH + sem-uniq-H = Functor≡ aoo aom where + aoo : (v : H .Node) → arb𝓓 ⟅ v ⟆ ≡ ıH $g v + aoo = (λ v i → arb𝓓-agree i $g v) + + aom-type : ∀ {v w} → (f : FH [ v , w ]) → Type _ + aom-type {v}{w} f = PathP (λ i → 𝓓 [ aoo v i , aoo w i ]) + (arb𝓓 ⟪ f ⟫) + (semH ⟪ f ⟫) + + aom-id : ∀ {v} → aom-type {v} idₑ + aom-id = arb𝓓 .F-id ◁ λ i → 𝓓 .id + + aom-seq : ∀ {v w x} → {f : FH [ v , w ]} {g : FH [ w , x ]} + → aom-type f + → aom-type g + → aom-type (f ⋆ₑ g) + aom-seq hypf hypg = arb𝓓 .F-seq _ _ ◁ λ i → hypf i ⋆⟨ 𝓓 ⟩ hypg i + ıϕp = eqToPath ıϕ + + aom-F : ∀ {v w} + → (e : FG [ v , w ]) + → PathP (λ i → 𝓓 [ (arb𝓓-agree i $g (ϕ v)) + , (arb𝓓-agree i $g (ϕ w)) ]) + (arb𝓓 ⟪ Fϕ ⟪ e ⟫ ⟫) + (transportEq (λ (f : G .Node → 𝓓 .ob) → 𝓓 [ f v , f w ]) + ıϕ + (𝓕 ⟪ semG ⟪ e ⟫ ⟫)) + aom-F {v}{w} e = + pathified ▷ eqToPath ( + substPath≡transport' + (λ (f : G .Node → 𝓓 .ob) → 𝓓 [ f v , f w ]) + (𝓕 ⟪ semG ⟪ e ⟫ ⟫) + ıϕ) + where + pathified : + PathP (λ i → 𝓓 [ arb𝓓-agree i $g ϕ v , arb𝓓-agree i $g ϕ w ]) + (arb𝓓 ⟪ Fϕ ⟪ e ⟫ ⟫) + (transport (λ i → 𝓓 [ ıϕp i v , ıϕp i w ]) + (𝓕 ⟪ semG ⟪ e ⟫ ⟫)) + pathified = toPathP⁻ (( + fromPathP⁻ lem' + ∙ cong (transport⁻ (λ i → 𝓓 [ arb𝓕 (~ i) ⟅ v ⟆ + , arb𝓕 (~ i) ⟅ w ⟆ ])) + (fromPathP⁻ lem𝓒) + ∙ sym (transportComposite + ((λ i → 𝓓 [ 𝓕 ⟅ arb𝓒-agree (~ i) $g v ⟆ + , 𝓕 ⟅ arb𝓒-agree (~ i) $g w ⟆ ])) + (λ i → 𝓓 [ arb𝓕 i ⟅ v ⟆ , arb𝓕 i ⟅ w ⟆ ]) + ((𝓕 ⟪ semG ⟪ e ⟫ ⟫))) + ∙ ((λ i → transport (substOf-sems-agreeϕ i) (𝓕 ⟪ semG ⟪ e ⟫ ⟫))) + ∙ transportComposite + (λ i → 𝓓 [ ıϕp i v , ıϕp i w ]) + (λ i → 𝓓 [ arb𝓓-agree (~ i) $g ϕ v + , arb𝓓-agree (~ i) $g ϕ w ]) + (𝓕 ⟪ semG ⟪ e ⟫ ⟫) + )) + where + lem' : PathP (λ i → 𝓓 [ arb𝓕 (~ i) ⟅ v ⟆ + , arb𝓕 (~ i) ⟅ w ⟆ ]) + (arb𝓓 ⟪ Fϕ ⟪ e ⟫ ⟫) + (𝓕 ⟪ arb𝓒 ⟪ e ⟫ ⟫) + lem' i = arb𝓕 (~ i) ⟪ e ⟫ + + lem𝓒 : PathP (λ i → 𝓓 [ 𝓕 ⟅ arb𝓒-agree i $g v ⟆ + , 𝓕 ⟅ arb𝓒-agree i $g w ⟆ ]) + (𝓕 ⟪ arb𝓒 ⟪ e ⟫ ⟫) + (𝓕 ⟪ semG ⟪ e ⟫ ⟫) + lem𝓒 i = 𝓕 ⟪ sem-uniq-G i ⟪ e ⟫ ⟫ + + substOf-sems-agreeϕ : + ((λ i → 𝓓 [ 𝓕 ⟅ arb𝓒-agree (~ i) $g v ⟆ + , 𝓕 ⟅ arb𝓒-agree (~ i) $g w ⟆ ]) + ∙ (λ i → 𝓓 [ arb𝓕 i ⟅ v ⟆ , arb𝓕 i ⟅ w ⟆ ])) + ≡ ((λ i → 𝓓 [ ıϕp i v , ıϕp i w ]) + ∙ (λ i → 𝓓 [ arb𝓓-agree (~ i) $g ϕ v + , arb𝓓-agree (~ i) $g ϕ w ])) + substOf-sems-agreeϕ = + sym (cong-∙ A (λ i x → 𝓕 ⟅ arb𝓒-agree (~ i) $g x ⟆) + λ i x → arb𝓕 i ⟅ x ⟆) + ∙ cong (cong A) + (Square→compPath λ i j x → arb𝓕-agree (~ i) j x) + ∙ cong-∙ A (λ i x → ıϕp i x) + (λ i x → arb𝓓-agree (~ i) $g ϕ x) where + the-type = (G .Node → 𝓓 .ob) + A = (λ (f : the-type) → 𝓓 [ f v , f w ]) + aom : ∀ {v w : H .Node} (f : FH [ v , w ]) → aom-type f + aom (↑ x) = λ i → arb𝓓-agree i <$g> x + aom idₑ = aom-id + aom (f ⋆ₑ g) = aom-seq (aom f) (aom g) + aom F⟪ x ⟫ = aom-F x + aom (⋆ₑIdL f i) = + isSet→SquareP + (λ i j → 𝓓 .isSetHom) + (aom-seq aom-id (aom f)) + (aom f) + (λ i → arb𝓓 ⟪ ⋆ₑIdL f i ⟫) + (λ i → (semH ⟪ ⋆ₑIdL f i ⟫)) + i + aom (⋆ₑIdR f i) = + isSet→SquareP (λ i j → 𝓓 .isSetHom) + (aom-seq (aom f) aom-id) + (aom f ) + (λ i → arb𝓓 ⟪ ⋆ₑIdR f i ⟫) + (λ i → semH ⟪ ⋆ₑIdR f i ⟫) + i + aom (⋆ₑAssoc f f₁ f₂ i) = + isSet→SquareP + (λ i j → 𝓓 .isSetHom) + (aom-seq (aom-seq (aom f) (aom f₁)) (aom f₂)) + (aom-seq (aom f) (aom-seq (aom f₁) (aom f₂))) + (λ i → arb𝓓 ⟪ ⋆ₑAssoc f f₁ f₂ i ⟫) + (λ i → semH ⟪ ⋆ₑAssoc f f₁ f₂ i ⟫) + i + aom (F-idₑ i) = + isSet→SquareP + (λ i j → 𝓓 .isSetHom) + (aom-F idₑ) + aom-id + (λ i → arb𝓓 ⟪ F-idₑ i ⟫) + (λ i → semH ⟪ F-idₑ i ⟫) + i + aom (F-seqₑ f g i) = + isSet→SquareP + (λ i j → 𝓓 .isSetHom) + (aom-F (f ⋆ₑ g)) + (aom-seq (aom-F f) (aom-F g)) + (λ i → arb𝓓 ⟪ F-seqₑ f g i ⟫) + (λ i → semH ⟪ F-seqₑ f g i ⟫) + i + aom (isSetFExp f f₁ x y i j) k = + isSet→SquareP + (λ i j → (isOfHLevelPathP {A = λ k → 𝓓 [ aoo _ k , aoo _ k ]} 2 + (𝓓 .isSetHom) + (arb𝓓 ⟪ isSetFExp f f₁ x y i j ⟫) + ((semH ⟪ isSetFExp f f₁ x y i j ⟫)))) + (λ j k → aom (x j) k) + (λ j k → aom (y j) k) + (λ i k → aom f k) + (λ i k → aom f₁ k) + i j k diff --git a/Cubical/Categories/Constructions/Lift.agda b/Cubical/Categories/Constructions/Lift.agda new file mode 100644 index 0000000000..2ed45fa913 --- /dev/null +++ b/Cubical/Categories/Constructions/Lift.agda @@ -0,0 +1,37 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Constructions.Lift where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels + +open import Cubical.Categories.Category +open import Cubical.Categories.Functor + +private + variable + ℓ ℓ' : Level + +open Category + +module _ (C : Category ℓ ℓ') (ℓ'' : Level) where + LiftHoms : Category ℓ (ℓ-max ℓ' ℓ'') + LiftHoms .ob = C .ob + LiftHoms .Hom[_,_] A B = Lift {j = ℓ''} (C [ A , B ]) + LiftHoms .id = lift (C .id) + LiftHoms ._⋆_ f g = lift (f .lower ⋆⟨ C ⟩ g .lower) + LiftHoms .⋆IdL f = cong lift (C .⋆IdL (f .lower)) + LiftHoms .⋆IdR f = cong lift (C .⋆IdR (f .lower)) + LiftHoms .⋆Assoc f g h = cong lift (C .⋆Assoc (f .lower) (g .lower) (h .lower)) + LiftHoms .isSetHom = isOfHLevelLift 2 (C .isSetHom) + + liftHoms : Functor C LiftHoms + liftHoms .Functor.F-ob = λ z → z + liftHoms .Functor.F-hom = lift + liftHoms .Functor.F-id = refl + liftHoms .Functor.F-seq f g = refl + + lowerHoms : Functor LiftHoms C + lowerHoms .Functor.F-ob = λ z → z + lowerHoms .Functor.F-hom = lower + lowerHoms .Functor.F-id = refl + lowerHoms .Functor.F-seq f g = refl diff --git a/Cubical/Categories/Constructions/Power.agda b/Cubical/Categories/Constructions/Power.agda new file mode 100644 index 0000000000..6c0359bad8 --- /dev/null +++ b/Cubical/Categories/Constructions/Power.agda @@ -0,0 +1,27 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Constructions.Power where + +open import Cubical.Foundations.Prelude + +open import Cubical.Categories.Category +open import Cubical.Categories.Constructions.Product +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets + +private + variable + ℓ ℓc ℓc' : Level + +open Category + +PowerCategory : (X : Type ℓ) (C : Category ℓc ℓc') → Category _ _ +PowerCategory X C = ΠC X (λ _ → C) + +PseudoYoneda : {C : Category ℓc ℓc'} + → Functor C (PowerCategory (C .ob) (SET ℓc')) +PseudoYoneda {C = C} = Π-intro _ (λ _ → SET _) λ a → C [ a ,-] + +isFaithfulPseudoYoneda : {C : Category ℓc ℓc'} + → Functor.isFaithful (PseudoYoneda {C = C}) +isFaithfulPseudoYoneda {C = C} x y f g p = + sym (C .⋆IdL f) ∙ (λ i → p i _ (C .id)) ∙ C .⋆IdL g diff --git a/Cubical/Categories/Constructions/Product.agda b/Cubical/Categories/Constructions/Product.agda index e249fe2ae5..45a3bb10b3 100644 --- a/Cubical/Categories/Constructions/Product.agda +++ b/Cubical/Categories/Constructions/Product.agda @@ -3,23 +3,38 @@ module Cubical.Categories.Constructions.Product where +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels + open import Cubical.Categories.Category.Base open import Cubical.Categories.Functor.Base -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Prelude private variable - ℓA ℓC ℓC' : Level + ℓA ℓC ℓC' ℓD ℓD' : Level open Category +open Functor + +module _ (A : Type ℓA) (catC : A → Category ℓC ℓC') where + ΠC : Category (ℓ-max ℓA ℓC) (ℓ-max ℓA ℓC') + ΠC .ob = (a : A) → ob (catC a) + ΠC .Hom[_,_] c c' = (a : A) → catC a [ c a , c' a ] + ΠC .id a = id (catC a) + ΠC ._⋆_ g f a = g a ⋆⟨ catC a ⟩ f a + ΠC .⋆IdL f = funExt λ a → ⋆IdL (catC a) (f a) + ΠC .⋆IdR f = funExt λ a → ⋆IdR (catC a) (f a) + ΠC .⋆Assoc h g f = funExt λ a → ⋆Assoc (catC a) (h a) (g a) (f a) + ΠC .isSetHom = isSetΠ (λ a → isSetHom (catC a)) + + Π-intro : {D : Category ℓD ℓD'} → (∀ (a : A) → Functor D (catC a)) → Functor D ΠC + Π-intro Fs .Functor.F-ob d a = Fs a ⟅ d ⟆ + Π-intro Fs .Functor.F-hom f a = Fs a ⟪ f ⟫ + Π-intro Fs .Functor.F-id = funExt (λ a → Fs a .F-id) + Π-intro Fs .Functor.F-seq f g = funExt (λ a → Fs a .F-seq f g) -ΠC : (A : Type ℓA) → (catC : A → Category ℓC ℓC') → Category (ℓ-max ℓA ℓC) (ℓ-max ℓA ℓC') -ob (ΠC A catC) = (a : A) → ob (catC a) -Hom[_,_] (ΠC A catC) c c' = (a : A) → catC a [ c a , c' a ] -id (ΠC A catC) a = id (catC a) -_⋆_ (ΠC A catC) g f a = g a ⋆⟨ catC a ⟩ f a -⋆IdL (ΠC A catC) f = funExt λ a → ⋆IdL (catC a) (f a) -⋆IdR (ΠC A catC) f = funExt λ a → ⋆IdR (catC a) (f a) -⋆Assoc (ΠC A catC) h g f = funExt λ a → ⋆Assoc (catC a) (h a) (g a) (f a) -isSetHom (ΠC A catC) = isSetΠ (λ a → isSetHom (catC a)) + πC : (a : A) → Functor ΠC (catC a) + πC a .Functor.F-ob = λ xs → xs a + πC a .Functor.F-hom = λ fs → fs a + πC a .Functor.F-id = refl + πC a .Functor.F-seq fs gs = refl diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda index 327fb95ede..eb3498dfe0 100644 --- a/Cubical/Categories/Instances/Functors.agda +++ b/Cubical/Categories/Instances/Functors.agda @@ -1,21 +1,34 @@ {-# OPTIONS --safe #-} +{- + Category whose objects are functors and morphisms are natural transformations. + + Includes the following + - isos in FUNCTOR are precisely the pointwise isos + - FUNCTOR C D is univalent when D is + - currying of functors + + TODO: show that currying of functors is an isomorphism. +-} + module Cubical.Categories.Instances.Functors where -open import Cubical.Categories.Category renaming (isIso to isIsoC) -open import Cubical.Categories.Functor.Base -open import Cubical.Categories.NaturalTransformation.Base -open import Cubical.Categories.NaturalTransformation.Properties -open import Cubical.Categories.Morphism open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.Properties open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Constructions.BinProduct +open import Cubical.Categories.Functor.Base +open import Cubical.Categories.Morphism +open import Cubical.Categories.NaturalTransformation.Base +open import Cubical.Categories.NaturalTransformation.Properties + private variable - ℓC ℓC' ℓD ℓD' : Level + ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where open Category @@ -102,3 +115,57 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where isUnivalentFUNCTOR isUnivD .univ _ _ = isEquiv[equivFunA≃B∘f]→isEquiv[f] _ FUNCTORIso≃NatIso (subst isEquiv (λ i p → Path→FUNCTORIso→NatIso p i) (Path≃NatIso isUnivD .snd)) + + appF : Functor (FUNCTOR ×C C) D + appF .F-ob (F , c) = F ⟅ c ⟆ + appF .F-hom {F , c} {G , d} (α , f) = α .N-ob d ∘⟨ D ⟩ F .F-hom f + appF .F-id {F , c} = + D .id ∘⟨ D ⟩ F .F-hom (C .id) ≡⟨ D .⋆IdR (F .F-hom (C .id)) ⟩ + F .F-hom (C .id) ≡⟨ F .F-id ⟩ + D .id ∎ + appF .F-seq {F , c}{G , d}{H , e} (α , f) (β , g ) = + (β .N-ob e ∘⟨ D ⟩ α .N-ob e) ∘⟨ D ⟩ F .F-hom (g ∘⟨ C ⟩ f) + ≡⟨ (λ i → (β .N-ob e ∘⟨ D ⟩ α .N-ob e) ∘⟨ D ⟩ F .F-seq f g i) ⟩ + (β .N-ob e ∘⟨ D ⟩ α .N-ob e) ∘⟨ D ⟩ (F .F-hom g ∘⟨ D ⟩ F .F-hom f) + ≡⟨ sym (D .⋆Assoc _ _ _) ⟩ + β .N-ob e ∘⟨ D ⟩ (α .N-ob e ∘⟨ D ⟩ (F .F-hom g ∘⟨ D ⟩ F .F-hom f)) + ≡⟨ (λ i → β .N-ob e + ∘⟨ D ⟩ D .⋆Assoc (F .F-hom f) (F .F-hom g) (α .N-ob e) i) ⟩ + β .N-ob e ∘⟨ D ⟩ ((α .N-ob e ∘⟨ D ⟩ F .F-hom g) ∘⟨ D ⟩ F .F-hom f) + ≡⟨ (λ i → β .N-ob e ∘⟨ D ⟩ α .N-hom g i ∘⟨ D ⟩ F .F-hom f) ⟩ + β .N-ob e ∘⟨ D ⟩ ((G .F-hom g ∘⟨ D ⟩ α .N-ob d) ∘⟨ D ⟩ F .F-hom f) + ≡⟨ (λ i → β .N-ob e + ∘⟨ D ⟩ D .⋆Assoc (F .F-hom f) (α .N-ob d) (G .F-hom g) (~ i) ) ⟩ + β .N-ob e ∘⟨ D ⟩ (G .F-hom g ∘⟨ D ⟩ (α .N-ob d ∘⟨ D ⟩ F .F-hom f)) + ≡⟨ D .⋆Assoc _ _ _ ⟩ + (β .N-ob e ∘⟨ D ⟩ G .F-hom g) ∘⟨ D ⟩ (α .N-ob d ∘⟨ D ⟩ F .F-hom f) ∎ + module _ (E : Category ℓE ℓE') where + λF : Functor (E ×C C) D → Functor E FUNCTOR + λF F .F-ob e .F-ob c = F ⟅ e , c ⟆ + λF F .F-ob e .F-hom f = F ⟪ (E .id) , f ⟫ + λF F .F-ob e .F-id = F .F-id + λF F .F-ob e .F-seq f g = + F ⟪ E .id , g ∘⟨ C ⟩ f ⟫ + ≡⟨ (λ i → F ⟪ (E .⋆IdL (E .id) (~ i)) , (g ∘⟨ C ⟩ f) ⟫) ⟩ + (F ⟪ (E .id ∘⟨ E ⟩ E .id) , g ∘⟨ C ⟩ f ⟫) + ≡⟨ F .F-seq (E .id , f) (E .id , g) ⟩ + (F ⟪ E .id , g ⟫ ∘⟨ D ⟩ F ⟪ E .id , f ⟫) ∎ + λF F .F-hom h .N-ob c = F ⟪ h , (C .id) ⟫ + λF F .F-hom h .N-hom f = + F ⟪ h , C .id ⟫ ∘⟨ D ⟩ F ⟪ E .id , f ⟫ ≡⟨ sym (F .F-seq _ _) ⟩ + F ⟪ h ∘⟨ E ⟩ E .id , C .id ∘⟨ C ⟩ f ⟫ + ≡⟨ (λ i → F ⟪ E .⋆IdL h i , C .⋆IdR f i ⟫) ⟩ + F ⟪ h , f ⟫ ≡⟨ (λ i → F ⟪ (E .⋆IdR h (~ i)) , (C .⋆IdL f (~ i)) ⟫) ⟩ + F ⟪ E .id ∘⟨ E ⟩ h , f ∘⟨ C ⟩ C .id ⟫ ≡⟨ F .F-seq _ _ ⟩ + F ⟪ E .id , f ⟫ ∘⟨ D ⟩ F ⟪ h , C .id ⟫ ∎ + λF F .F-id = makeNatTransPath (funExt λ c → F .F-id) + λF F .F-seq f g = makeNatTransPath (funExt lem) where + lem : (c : C .ob) → + F ⟪ g ∘⟨ E ⟩ f , C .id ⟫ ≡ + F ⟪ g , C .id ⟫ ∘⟨ D ⟩ F ⟪ f , C .id ⟫ + lem c = + F ⟪ g ∘⟨ E ⟩ f , C .id ⟫ + ≡⟨ (λ i → F ⟪ (g ∘⟨ E ⟩ f) , (C .⋆IdR (C .id) (~ i)) ⟫) ⟩ + F ⟪ g ∘⟨ E ⟩ f , C .id ∘⟨ C ⟩ C .id ⟫ + ≡⟨ F .F-seq (f , C .id) (g , C .id) ⟩ + (F ⟪ g , C .id ⟫) ∘⟨ D ⟩ (F ⟪ f , C .id ⟫) ∎ diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index fb598e7849..fd0589da27 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -47,6 +47,13 @@ _[_,-] : (C : Category ℓ ℓ') → (c : C .ob)→ Functor C (SET ℓ') (C [ c ,-]) .F-id = funExt λ _ → C .⋆IdR _ (C [ c ,-]) .F-seq _ _ = funExt λ _ → sym (C .⋆Assoc _ _ _) +-- Lift functor +LiftF : Functor (SET ℓ) (SET (ℓ-max ℓ ℓ')) +LiftF {ℓ}{ℓ'} .F-ob A = (Lift {ℓ}{ℓ'} (A .fst)) , isOfHLevelLift 2 (A .snd) +LiftF .F-hom f x = lift (f (x .lower)) +LiftF .F-id = refl +LiftF .F-seq f g = funExt λ x → refl + module _ {C : Category ℓ ℓ'} {F : Functor C (SET ℓ')} where open NatTrans diff --git a/Cubical/Categories/Limits/Terminal.agda b/Cubical/Categories/Limits/Terminal.agda index 438ac83c10..41d73e6f25 100644 --- a/Cubical/Categories/Limits/Terminal.agda +++ b/Cubical/Categories/Limits/Terminal.agda @@ -4,14 +4,15 @@ module Cubical.Categories.Limits.Terminal where open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.HITs.PropositionalTruncation.Base - open import Cubical.Data.Sigma open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Isomorphism private variable - ℓ ℓ' : Level + ℓ ℓ' ℓc ℓc' ℓd ℓd' : Level module _ (C : Category ℓ ℓ') where open Category C @@ -45,13 +46,20 @@ module _ (C : Category ℓ ℓ') where open isIso - -- Objects that are initial are isomorphic. + -- Objects that are terminal are isomorphic. terminalToIso : (x y : Terminal) → CatIso C (terminalOb x) (terminalOb y) terminalToIso x y .fst = terminalArrow y (terminalOb x) terminalToIso x y .snd .inv = terminalArrow x (terminalOb y) terminalToIso x y .snd .sec = terminalEndoIsId y _ terminalToIso x y .snd .ret = terminalEndoIsId x _ + isoToTerminal : ∀ (x : Terminal) y → CatIso C (terminalOb x) y → isTerminal y + isoToTerminal x y x≅y y' .fst = x≅y .fst ∘⟨ C ⟩ terminalArrow x y' + isoToTerminal x y x≅y y' .snd f = + sym (⋆InvRMove + (invIso x≅y) + (sym (terminalArrowUnique {T = x} (invIso x≅y .fst ∘⟨ C ⟩ f)))) + open isUnivalent -- The type of terminal objects of a univalent category is a proposition, @@ -59,3 +67,17 @@ module _ (C : Category ℓ ℓ') where isPropTerminal : (hC : isUnivalent C) → isProp Terminal isPropTerminal hC x y = Σ≡Prop isPropIsTerminal (CatIsoToPath hC (terminalToIso x y)) + +preservesTerminals : ∀ (C : Category ℓc ℓc')(D : Category ℓd ℓd') + → Functor C D + → Type (ℓ-max (ℓ-max (ℓ-max ℓc ℓc') ℓd) ℓd') +preservesTerminals C D F = ∀ (term : Terminal C) → isTerminal D (F ⟅ term .fst ⟆) + +preserveAnyTerminal→PreservesTerminals : ∀ (C : Category ℓc ℓc')(D : Category ℓd ℓd') + → (F : Functor C D) + → (term : Terminal C) → isTerminal D (F ⟅ term .fst ⟆) + → preservesTerminals C D F +preserveAnyTerminal→PreservesTerminals C D F term D-preserves-term term' = + isoToTerminal D + ((F ⟅ term .fst ⟆) , D-preserves-term) (F ⟅ term' .fst ⟆) + (F-Iso {F = F} (terminalToIso C term term')) diff --git a/Cubical/Categories/NaturalTransformation/Properties.agda b/Cubical/Categories/NaturalTransformation/Properties.agda index d71850ec8b..1d105278b4 100644 --- a/Cubical/Categories/NaturalTransformation/Properties.agda +++ b/Cubical/Categories/NaturalTransformation/Properties.agda @@ -12,13 +12,14 @@ open import Cubical.Foundations.Isomorphism renaming (iso to iIso) open import Cubical.Data.Sigma open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Functor.Base +open import Cubical.Categories.Functor.Properties open import Cubical.Categories.Morphism open import Cubical.Categories.Isomorphism open import Cubical.Categories.NaturalTransformation.Base private variable - ℓC ℓC' ℓD ℓD' : Level + ℓB ℓB' ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level open isIsoC open NatIso @@ -129,3 +130,45 @@ module _ Path≃NatIso : (F ≡ G) ≃ NatIso F G Path≃NatIso = isoToEquiv Iso-Path-NatIso +module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where + seqNatIso : {F G H : Functor C D} → NatIso F G → NatIso G H → NatIso F H + seqNatIso ı ı' .trans = seqTrans (ı .trans) (ı' .trans) + seqNatIso ı ı' .nIso x .inv = ı' .nIso x .inv ⋆⟨ D ⟩ ı .nIso x .inv + seqNatIso ı ı' .nIso x .sec = + D .⋆Assoc _ _ _ + ∙ cong (_⋆_ D (ı' .nIso x .inv)) + (sym (D .⋆Assoc _ _ _) + ∙ cong (D ∘ ı' .trans .N-ob x) (ı .nIso x .sec) + ∙ D .⋆IdL (ı' .trans .N-ob x)) + ∙ ı' .nIso x .sec + seqNatIso ı ı' .nIso x .ret = + (sym (D .⋆Assoc _ _ _)) + ∙ cong (_∘_ D (ı .nIso x .inv)) + (D .⋆Assoc _ _ _ + ∙ cong (D ⋆ ı .trans .N-ob x) (ı' .nIso x .ret) + ∙ D .⋆IdR (ı .trans .N-ob x)) + ∙ ı .nIso x .ret + + CAT⋆IdR : {F : Functor C D} → NatIso (Id ∘F F) F + CAT⋆IdR {F} .trans .N-ob = idTrans F .N-ob + CAT⋆IdR {F} .trans .N-hom = idTrans F .N-hom + CAT⋆IdR {F} .nIso = idNatIso F .nIso + +module _ {B : Category ℓB ℓB'}{C : Category ℓC ℓC'}{D : Category ℓD ℓD'} where + _∘ʳi_ : ∀ (K : Functor C D) → {G H : Functor B C} (β : NatIso G H) + → NatIso (K ∘F G) (K ∘F H) + _∘ʳi_ K β .trans = K ∘ʳ β .trans + _∘ʳi_ K β .nIso x = preserveIsosF {F = K} (β .trans .N-ob _ , β .nIso x) .snd + + open Functor + _∘ˡi_ : ∀ (K : Functor B C) → {G H : Functor C D} (β : NatIso G H) + → NatIso (G ∘F K) (H ∘F K) + _∘ˡi_ K β .trans = β .trans ∘ˡ K + _∘ˡi_ K β .nIso b = β .nIso (K ⟅ b ⟆) + + CAT⋆Assoc : {E : Category ℓE ℓE'} + (F : Functor B C)(G : Functor C D)(H : Functor D E) + → NatIso (H ∘F (G ∘F F)) ((H ∘F G) ∘F F) + CAT⋆Assoc F G H .trans .N-ob = idTrans ((H ∘F G) ∘F F) .N-ob + CAT⋆Assoc F G H .trans .N-hom = idTrans ((H ∘F G) ∘F F) .N-hom + CAT⋆Assoc F G H .nIso = idNatIso ((H ∘F G) ∘F F) .nIso diff --git a/Cubical/Categories/Presheaf.agda b/Cubical/Categories/Presheaf.agda index 4fe1dc15c2..932e4dbbf4 100644 --- a/Cubical/Categories/Presheaf.agda +++ b/Cubical/Categories/Presheaf.agda @@ -4,4 +4,7 @@ module Cubical.Categories.Presheaf where open import Cubical.Categories.Presheaf.Base public open import Cubical.Categories.Presheaf.KanExtension public +open import Cubical.Categories.Presheaf.Morphism public open import Cubical.Categories.Presheaf.Properties public +open import Cubical.Categories.Presheaf.Representable public + diff --git a/Cubical/Categories/Presheaf/Base.agda b/Cubical/Categories/Presheaf/Base.agda index cd126efd29..7d84647e9f 100644 --- a/Cubical/Categories/Presheaf/Base.agda +++ b/Cubical/Categories/Presheaf/Base.agda @@ -4,9 +4,9 @@ module Cubical.Categories.Presheaf.Base where open import Cubical.Foundations.Prelude open import Cubical.Categories.Category -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Instances.Functors open import Cubical.Categories.Functor.Base +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.Instances.Sets private variable @@ -20,5 +20,28 @@ PresheafCategory : Category ℓ ℓ' → (ℓS : Level) (ℓ-max (ℓ-max ℓ ℓ') ℓS) PresheafCategory C ℓS = FUNCTOR (C ^op) (SET ℓS) -isUnivalentPresheafCategory : {C : Category ℓ ℓ'} → isUnivalent (PresheafCategory C ℓS) +isUnivalentPresheafCategory : {C : Category ℓ ℓ'} + → isUnivalent (PresheafCategory C ℓS) isUnivalentPresheafCategory = isUnivalentFUNCTOR _ _ isUnivalentSET + +open Category +open Functor + +action : ∀ (C : Category ℓ ℓ') → (P : Presheaf C ℓS) + → {a b : C .ob} → C [ a , b ] → fst (P ⟅ b ⟆) → fst (P ⟅ a ⟆) +action C P = P .F-hom + +-- Convenient notation for naturality +syntax action C P f ϕ = ϕ ∘ᴾ⟨ C , P ⟩ f + +∘ᴾId : ∀ (C : Category ℓ ℓ') → (P : Presheaf C ℓS) → {a : C .ob} + → (ϕ : fst (P ⟅ a ⟆)) + → ϕ ∘ᴾ⟨ C , P ⟩ C .id ≡ ϕ +∘ᴾId C P ϕ i = P .F-id i ϕ + +∘ᴾAssoc : ∀ (C : Category ℓ ℓ') → (P : Presheaf C ℓS) → {a b c : C .ob} + → (ϕ : fst (P ⟅ c ⟆)) + → (f : C [ b , c ]) + → (g : C [ a , b ]) + → ϕ ∘ᴾ⟨ C , P ⟩ (f ∘⟨ C ⟩ g) ≡ (ϕ ∘ᴾ⟨ C , P ⟩ f) ∘ᴾ⟨ C , P ⟩ g +∘ᴾAssoc C P ϕ f g i = P .F-seq f g i ϕ diff --git a/Cubical/Categories/Presheaf/Morphism.agda b/Cubical/Categories/Presheaf/Morphism.agda new file mode 100644 index 0000000000..ee86bf91ea --- /dev/null +++ b/Cubical/Categories/Presheaf/Morphism.agda @@ -0,0 +1,96 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Presheaf.Morphism where + +open import Cubical.Foundations.Prelude + +open import Cubical.Data.Sigma + +open import Cubical.Categories.Category +open import Cubical.Categories.Constructions.Elements +open import Cubical.Categories.Constructions.Lift +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Isomorphism +open import Cubical.Categories.Limits +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Presheaf.Base +open import Cubical.Categories.Presheaf.Representable + +{- + + Given two presheaves P and Q on the same category C, a morphism + between them is a natural transformation. Here we generalize this to + situations where P and Q are presheaves on *different* + categories. This is equivalent to the notion of morphism of + fibrations if viewing P and Q as discrete fibrations. + + Given a functor F : C → D, a presheaf P on C and a presheaf Q on D, + we can define a homomorphism from P to Q over F as a natural + transformation from P to Q o F^op. (if we had implicit cumulativity) + + These are the homs of a 2-category of presheaves displayed over the + 2-category of categories. + +-} +private + variable + ℓc ℓc' ℓd ℓd' ℓp ℓq : Level + +open Category +open Contravariant +open Functor +open NatTrans +open UniversalElement + +module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'} + (F : Functor C D) + (P : Presheaf C ℓp) + (Q : Presheaf D ℓq) where + PshHom : Type (ℓ-max (ℓ-max (ℓ-max ℓc ℓc') ℓp) ℓq) + PshHom = + PresheafCategory C (ℓ-max ℓp ℓq) + [ LiftF {ℓp}{ℓq} ∘F P , LiftF {ℓq}{ℓp} ∘F Q ∘F (F ^opF) ] + + module _ (h : PshHom) where + -- This should define a functor on the category of elements + pushElt : Elementᴾ {C = C} P → Elementᴾ {C = D} Q + pushElt (A , η) = (F ⟅ A ⟆) , (h .N-ob A (lift η) .lower) + + pushEltNat : ∀ {B : C .ob} (η : Elementᴾ {C = C} P) (f : C [ B , η .fst ]) + → (pushElt η .snd ∘ᴾ⟨ D , Q ⟩ F .F-hom f) + ≡ pushElt (B , η .snd ∘ᴾ⟨ C , P ⟩ f) .snd + pushEltNat η f i = h .N-hom f (~ i) (lift (η .snd)) .lower + + pushEltF : Functor (∫ᴾ_ {C = C} P) (∫ᴾ_ {C = D} Q) + pushEltF .F-ob = pushElt + pushEltF .F-hom {x}{y} (f , commutes) = F .F-hom f , sym ( + pushElt _ .snd ∘ᴾ⟨ D , Q ⟩ F .F-hom f + ≡⟨ pushEltNat y f ⟩ + pushElt (_ , y .snd ∘ᴾ⟨ C , P ⟩ f) .snd + ≡⟨ cong (λ a → pushElt a .snd) (ΣPathP (refl , (sym commutes))) ⟩ + pushElt x .snd ∎) + pushEltF .F-id = Σ≡Prop (λ x → (Q ⟅ _ ⟆) .snd _ _) (F .F-id) + pushEltF .F-seq f g = + Σ≡Prop ((λ x → (Q ⟅ _ ⟆) .snd _ _)) (F .F-seq (f .fst) (g .fst)) + + preservesRepresentation : ∀ (η : UniversalElement C P) + → Type (ℓ-max (ℓ-max ℓd ℓd') ℓq) + preservesRepresentation η = isUniversal D Q (η' .fst) (η' .snd) + where η' = pushElt (η .vertex , η .element) + + preservesRepresentations : Type _ + preservesRepresentations = ∀ η → preservesRepresentation η + + -- If C and D are univalent then this follows by representability + -- being a Prop. But even in non-univalent categories it follows + -- by uniqueness of representables up to unique isomorphism + preservesAnyRepresentation→preservesAllRepresentations : + ∀ η → preservesRepresentation η → preservesRepresentations + preservesAnyRepresentation→preservesAllRepresentations η preserves-η η' = + isTerminalToIsUniversal D Q + (preserveAnyTerminal→PreservesTerminals (∫ᴾ_ {C = C} P) + (∫ᴾ_ {C = D} Q) + pushEltF + (universalElementToTerminalElement C P η) + (isUniversalToIsTerminal D Q _ _ preserves-η) + (universalElementToTerminalElement C P η')) diff --git a/Cubical/Categories/Presheaf/Properties.agda b/Cubical/Categories/Presheaf/Properties.agda index ceb70cbd66..a9737470c3 100644 --- a/Cubical/Categories/Presheaf/Properties.agda +++ b/Cubical/Categories/Presheaf/Properties.agda @@ -3,6 +3,7 @@ module Cubical.Categories.Presheaf.Properties where open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Constructions.Lift open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.Functors @@ -23,6 +24,7 @@ import Cubical.Functions.Fibration as Fibration private variable ℓ ℓ' : Level + ℓS ℓS' : Level e e' : Level @@ -385,3 +387,9 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) preshSlice≃preshElem .isEquiv .η .nIso = ηIso preshSlice≃preshElem .isEquiv .ε .trans = εTrans preshSlice≃preshElem .isEquiv .ε .nIso = εIso + + +-- Isomorphism between presheaves of different levels +PshIso : (C : Category ℓ ℓ') (P : Presheaf C ℓS) (Q : Presheaf C ℓS') → Type _ +PshIso {ℓS = ℓS}{ℓS' = ℓS'} C P Q = + NatIso (LiftF {ℓ = ℓS}{ℓ' = ℓS'} ∘F P) (LiftF {ℓ = ℓS'}{ℓ' = ℓS} ∘F Q) diff --git a/Cubical/Categories/Presheaf/Representable.agda b/Cubical/Categories/Presheaf/Representable.agda new file mode 100644 index 0000000000..95e99c9007 --- /dev/null +++ b/Cubical/Categories/Presheaf/Representable.agda @@ -0,0 +1,196 @@ +{-# OPTIONS --safe #-} +{- + + This file defines 3 equivalent formulations of when a presheaf P is + representable: + + 1. When there is a natural isomorphism with some representable C [-, A ] + + 2. When there is a terminal element of the category of elements of P + + 3. When there is a universal element η ∈ P A, i.e., that composing with + η is an equivalence between P B and C [ B , A ]. + + The equivalence between 2 and 3 is mostly currying/symmetry of + equations. The equivalence between 1 and 3 follows from the Yoneda + lemma. + + 3 is the most convenient to construct in applications and so is + implemented with a custom record type UniversalElement and is + generally preferable when formulating universal properties. + +-} +module Cubical.Categories.Presheaf.Representable where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism + +open import Cubical.Data.Sigma +open import Cubical.HITs.PropositionalTruncation.Base +open import Cubical.Reflection.RecordEquiv + +open import Cubical.Categories.Category renaming (isIso to isIsoC) +open import Cubical.Categories.Constructions.Elements +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Limits +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Presheaf.Base +open import Cubical.Categories.Presheaf.Properties +open import Cubical.Categories.Yoneda + +private + variable ℓ ℓ' : Level + +open Category +open Contravariant +open NatIso +open isIsoC + +-- | A representation of a presheaf is an object whose image under the +-- | Yoneda embedding is isomorphic to P +-- | We define only the maximally universe polymorphic version, the +-- | Lifts don't appear in practice because we usually use universal +-- | elements instead +module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where + Representation : Type (ℓ-max (ℓ-max ℓo (ℓ-suc ℓh)) (ℓ-suc ℓp)) + Representation = + Σ[ A ∈ C .ob ] PshIso C (C [-, A ]) P + + Representable : Type (ℓ-max (ℓ-max ℓo (ℓ-suc ℓh)) (ℓ-suc ℓp)) + Representable = ∥ Representation ∥₁ + + Elements = ∫ᴾ_ {C = C} P + + TerminalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) + TerminalElement = Terminal Elements + + hasTerminalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) + hasTerminalElement = ∥ TerminalElement ∥₁ + + isUniversal : (vertex : C .ob) (element : (P ⟅ vertex ⟆) .fst) + → Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) + isUniversal vertex element = + ∀ A → isEquiv λ (f : C [ A , vertex ]) → element ∘ᴾ⟨ C , P ⟩ f + + isPropIsUniversal : ∀ vertex element → isProp (isUniversal vertex element) + isPropIsUniversal vertex element = isPropΠ (λ _ → isPropIsEquiv _) + + record UniversalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) where + field + vertex : C .ob + element : (P ⟅ vertex ⟆) .fst + universal : isUniversal vertex element + + unquoteDecl UniversalElementIsoΣ = + declareRecordIsoΣ UniversalElementIsoΣ (quote UniversalElement) + + hasUniversalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) + hasUniversalElement = ∥ UniversalElement ∥₁ + + open UniversalElement + + -- | The equivalence between Representation and UniversalElement is + -- | a corollary of the Yoneda lemma + representationToUniversalElement : Representation → UniversalElement + representationToUniversalElement repr .vertex = repr .fst + representationToUniversalElement repr .element = + Iso.fun (yonedaᴾ* {C = C} P (repr .fst)) (repr .snd .trans) + representationToUniversalElement repr .universal A = + transport (λ i → isEquiv (lem i)) (isoToIsEquiv anIso) + where + lem : + Path (C [ A , repr .fst ] → _) + (λ f → (repr .snd .trans ⟦ A ⟧) (lift f) .lower) + (λ f → (Iso.inv (yonedaᴾ* {C = C} P (repr .fst)) + (Iso.fun (yonedaᴾ* P (repr .fst)) + (repr .snd .trans)) ⟦ A ⟧) + (lift f) .lower) + lem = funExt (λ f i → + (yonedaᴾ* {C = C} P (repr .fst) + .Iso.leftInv (repr .snd .trans) (~ i) ⟦ A ⟧) + (lift f) .lower) + + anIso : Iso (C [ A , repr .fst ]) (fst (Functor.F-ob P A)) + anIso .Iso.fun f = (repr .snd .trans ⟦ A ⟧) (lift f) .lower + anIso .Iso.inv p = repr .snd .nIso A .inv (lift p) .lower + anIso .Iso.rightInv b = + cong lower (funExt⁻ (repr .snd .nIso A .sec) (lift b)) + anIso .Iso.leftInv a = + cong lower (funExt⁻ (repr .snd .nIso A .ret) (lift a)) + + universalElementToRepresentation : UniversalElement → Representation + universalElementToRepresentation η .fst = η .vertex + universalElementToRepresentation η .snd .trans = + yonedaᴾ* {C = C} P (η .vertex) .Iso.inv (η .element) + universalElementToRepresentation η .snd .nIso A .inv ϕ = + lift (invIsEq (η .universal A) (ϕ .lower)) + universalElementToRepresentation η .snd .nIso A .sec = funExt (λ ϕ → + cong lift (secIsEq (η .universal A) (ϕ .lower))) + universalElementToRepresentation η .snd .nIso A .ret = funExt (λ f → + cong lift (retIsEq (η .universal A) (f .lower))) + + Representation≅UniversalElement : Iso Representation UniversalElement + Representation≅UniversalElement .Iso.fun = representationToUniversalElement + Representation≅UniversalElement .Iso.inv = universalElementToRepresentation + Representation≅UniversalElement .Iso.rightInv η = + isoFunInjective UniversalElementIsoΣ _ _ + (ΣPathP (refl , (Σ≡Prop (λ _ → isPropIsUniversal _ _) + (yonedaᴾ* {C = C} P (η .vertex) .Iso.rightInv (η .element))))) + Representation≅UniversalElement .Iso.leftInv repr = + ΣPathP (refl , + (NatIso≡ (cong NatTrans.N-ob + (yonedaᴾ* {C = C} P (repr .fst) .Iso.leftInv (repr .snd .trans))))) + + isTerminalToIsUniversal : ∀ {η : Elementᴾ {C = C} P} + → isTerminal Elements η → isUniversal (η .fst) (η .snd) + isTerminalToIsUniversal {η} term A .equiv-proof ϕ .fst .fst = + term (_ , ϕ) .fst .fst + isTerminalToIsUniversal {η} term A .equiv-proof ϕ .fst .snd = + sym (term (_ , ϕ) .fst .snd) + isTerminalToIsUniversal {η} term A .equiv-proof ϕ .snd (f , commutes) = + Σ≡Prop (λ _ → (P ⟅ A ⟆) .snd _ _) + (cong fst (term (A , ϕ) .snd (f , sym commutes))) + + isUniversalToIsTerminal : + ∀ (vertex : C .ob) (element : (P ⟅ vertex ⟆) .fst) + → isUniversal vertex element + → isTerminal Elements (vertex , element) + isUniversalToIsTerminal vertex element universal ϕ .fst .fst = + universal _ .equiv-proof (ϕ .snd) .fst .fst + isUniversalToIsTerminal vertex element universal ϕ .fst .snd = + sym (universal _ .equiv-proof (ϕ .snd) .fst .snd) + isUniversalToIsTerminal vertex element universal ϕ .snd (f , commutes) = + Σ≡Prop + (λ _ → (P ⟅ _ ⟆) .snd _ _) + (cong fst (universal _ .equiv-proof (ϕ .snd) .snd (f , sym commutes))) + + terminalElementToUniversalElement : TerminalElement → UniversalElement + terminalElementToUniversalElement η .vertex = η .fst .fst + terminalElementToUniversalElement η .element = η .fst .snd + terminalElementToUniversalElement η .universal = + isTerminalToIsUniversal (η .snd) + + universalElementToTerminalElement : UniversalElement → TerminalElement + universalElementToTerminalElement η .fst .fst = η .vertex + universalElementToTerminalElement η .fst .snd = η .element + universalElementToTerminalElement η .snd = + isUniversalToIsTerminal (η .vertex) (η .element) (η .universal) + + TerminalElement≅UniversalElement : Iso TerminalElement UniversalElement + TerminalElement≅UniversalElement .Iso.fun = terminalElementToUniversalElement + TerminalElement≅UniversalElement .Iso.inv = universalElementToTerminalElement + TerminalElement≅UniversalElement .Iso.rightInv η = + isoFunInjective UniversalElementIsoΣ _ _ + (ΣPathP (refl , (Σ≡Prop (λ _ → isPropIsUniversal _ _) refl))) + TerminalElement≅UniversalElement .Iso.leftInv η = + Σ≡Prop (isPropIsTerminal Elements) refl + + Representation≅TerminalElement : Iso Representation TerminalElement + Representation≅TerminalElement = + compIso + Representation≅UniversalElement + (invIso TerminalElement≅UniversalElement) diff --git a/Cubical/Categories/UnderlyingGraph.agda b/Cubical/Categories/UnderlyingGraph.agda new file mode 100644 index 0000000000..1d4fe60d35 --- /dev/null +++ b/Cubical/Categories/UnderlyingGraph.agda @@ -0,0 +1,56 @@ +{-# OPTIONS --safe #-} + +module Cubical.Categories.UnderlyingGraph where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels + +open import Cubical.Data.Graph.Base +open import Cubical.Data.Sigma + +open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor +open import Cubical.Categories.Isomorphism +open import Cubical.Categories.Morphism +open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧) + +private + variable + ℓc ℓc' ℓd ℓd' ℓe ℓe' ℓg ℓg' ℓh ℓh' : Level + +open Category +open isIso +open Functor +open NatIso hiding (sqRL; sqLL) +open NatTrans + +-- Underlying graph of a category +Cat→Graph : ∀ {ℓc ℓc'} (𝓒 : Category ℓc ℓc') → Graph ℓc ℓc' +Cat→Graph 𝓒 .Node = 𝓒 .ob +Cat→Graph 𝓒 .Edge = 𝓒 .Hom[_,_] + +Functor→GraphHom : ∀ {ℓc ℓc' ℓd ℓd'} {𝓒 : Category ℓc ℓc'} {𝓓 : Category ℓd ℓd'} + (F : Functor 𝓒 𝓓) → GraphHom (Cat→Graph 𝓒) (Cat→Graph 𝓓) +Functor→GraphHom F ._$g_ = Functor.F-ob F +Functor→GraphHom F ._<$g>_ = Functor.F-hom F + +module _ (G : Graph ℓg ℓg') (𝓒 : Category ℓc ℓc') where + -- Interpretation of a graph in a category + Interp : Type _ + Interp = GraphHom G (Cat→Graph 𝓒) +_⋆Interp_ : ∀ {G : Graph ℓg ℓg'} + {𝓒 : Category ℓc ℓc'} + {𝓓 : Category ℓd ℓd'} + (ı : Interp G 𝓒) + (F : Functor 𝓒 𝓓) + → Interp G 𝓓 +(ı ⋆Interp F) ._$g_ x = Functor.F-ob F (ı $g x) +(ı ⋆Interp F) ._<$g>_ e = Functor.F-hom F (ı <$g> e) + +_∘Interp_ : ∀ {G : Graph ℓg ℓg'} + {𝓒 : Category ℓc ℓc'} + {𝓓 : Category ℓd ℓd'} + (F : Functor 𝓒 𝓓) + (ı : Interp G 𝓒) + → Interp G 𝓓 +F ∘Interp ı = ı ⋆Interp F diff --git a/Cubical/Categories/Yoneda.agda b/Cubical/Categories/Yoneda.agda index 5a4b1b9f64..ff27bde20e 100644 --- a/Cubical/Categories/Yoneda.agda +++ b/Cubical/Categories/Yoneda.agda @@ -11,11 +11,12 @@ open import Cubical.Foundations.Equiv open import Cubical.HITs.PropositionalTruncation open import Cubical.Categories.Category +open import Cubical.Categories.Constructions.Lift open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.Functors open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.Functor -open import Cubical.Categories.Presheaf +open import Cubical.Categories.Presheaf.Base private variable @@ -43,8 +44,8 @@ module _ {C : Category ℓ ℓ'} where ϕ : natType → setType ϕ α = (α ⟦ _ ⟧) (C .id) - -- takes an element x of F c and sends it to the (only) natural transformation - -- which takes the identity to x + -- takes an element x of F c and sends it to the (only) natural + -- transformation which takes the identity to x Ψ : setType → natType Ψ x .N-ob c = λ f → (F ⟪ f ⟫) x Ψ x .N-hom g @@ -57,7 +58,8 @@ module _ {C : Category ℓ ℓ'} where theIso .fun = ϕ theIso .inv = Ψ theIso .rightInv x i = F .F-id i x - theIso .leftInv α@(natTrans αo αh) = NatTrans-≡-intro (sym αo≡βo) (symP αh≡βh) + theIso .leftInv α@(natTrans αo αh) = + NatTrans-≡-intro (sym αo≡βo) (symP αh≡βh) where β = Ψ (ϕ α) βo = β .N-ob @@ -68,7 +70,8 @@ module _ {C : Category ℓ ℓ'} where αo≡βo : αo ≡ βo αo≡βo = funExt λ x → funExt λ f → αo x f - ≡[ i ]⟨ αo x (C .⋆IdL f (~ i)) ⟩ -- expand into the bottom left of the naturality diagram + -- expand into the bottom left of the naturality diagram + ≡[ i ]⟨ αo x (C .⋆IdL f (~ i)) ⟩ αo x (C .id ⋆⟨ C ⟩ f) ≡[ i ]⟨ αh f i (C .id) ⟩ -- apply naturality (F ⟪ f ⟫) ((αo _) (C .id)) @@ -83,7 +86,9 @@ module _ {C : Category ℓ ℓ'} where αh≡βh = isPropHomP αh βh αo≡βo where isProp-hom : (ϕ : NOType) → isProp (NHType ϕ) - isProp-hom γ = isPropImplicitΠ2 λ x y → isPropΠ λ f → isSetHom (SET _) {x = (C [ c , x ]) , C .isSetHom } {F ⟅ y ⟆} _ _ + isProp-hom γ = isPropImplicitΠ2 λ x y → isPropΠ λ f → + isSetHom (SET _) + {x = (C [ c , x ]) , C .isSetHom } {F ⟅ y ⟆} _ _ isPropHomP : isOfHLevelDep 1 (λ ηo → NHType ηo) isPropHomP = isOfHLevel→isOfHLevelDep 1 λ a → isProp-hom a @@ -96,7 +101,8 @@ module _ {C : Category ℓ ℓ'} where -- where ϕ takes a natural transformation to its representing element yonedaIsNaturalInFunctor : ∀ {F G : Functor C (SET ℓ')} (c : C .ob) → (β : F ⇒ G) - → (fun (yoneda G c) ◍ compTrans β) ≡ (β ⟦ c ⟧ ◍ fun (yoneda F c)) + → (fun (yoneda G c) ◍ compTrans β) + ≡ (β ⟦ c ⟧ ◍ fun (yoneda F c)) yonedaIsNaturalInFunctor {F = F} {G} c β = funExt λ α → refl -- in the object @@ -120,6 +126,88 @@ module _ {C : Category ℓ ℓ'} where ((F ⟪ f ⟫) ◍ yoneda F c .fun) α ∎) +-- Yoneda for contravariant functors +module _ {C : Category ℓ ℓ'} where + open Category + import Cubical.Categories.NaturalTransformation + open NatTrans + yonedaᴾ : (F : Functor (C ^op) (SET ℓ')) + → (c : C .ob) + → Iso ((FUNCTOR (C ^op) (SET ℓ')) [ C [-, c ] , F ]) (fst (F ⟅ c ⟆)) + yonedaᴾ F c = + ((FUNCTOR (C ^op) (SET ℓ')) [ C [-, c ] , F ]) Iso⟨ the-iso ⟩ + FUNCTOR (C ^op) (SET ℓ') [ (C ^op) [ c ,-] , F ] Iso⟨ yoneda F c ⟩ + (fst (F ⟅ c ⟆)) ∎Iso where + + to : FUNCTOR (C ^op) (SET ℓ') [ C [-, c ] , F ] + → FUNCTOR (C ^op) (SET ℓ') [ (C ^op) [ c ,-] , F ] + to α = natTrans (α .N-ob) (α .N-hom) + + fro : FUNCTOR (C ^op) (SET ℓ') [ (C ^op) [ c ,-] , F ] + → FUNCTOR (C ^op) (SET ℓ') [ C [-, c ] , F ] + fro β = natTrans (β .N-ob) (β .N-hom) + + the-iso : Iso (FUNCTOR (C ^op) (SET ℓ') [ C [-, c ] , F ]) + (FUNCTOR (C ^op) (SET ℓ') [ (C ^op) [ c ,-] , F ]) + the-iso = iso to fro (λ b → refl) λ a → refl + +-- A more universe-polymorphic Yoneda lemma +yoneda* : {C : Category ℓ ℓ'}(F : Functor C (SET ℓ'')) + → (c : Category.ob C) + → Iso ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-]) + , LiftF {ℓ''}{ℓ'} ∘F F ]) + (fst (F ⟅ c ⟆)) +yoneda* {ℓ}{ℓ'}{ℓ''}{C} F c = + ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-]) + , LiftF {ℓ''}{ℓ'} ∘F F ]) + Iso⟨ the-iso ⟩ + ((FUNCTOR (LiftHoms C ℓ'') + (SET (ℓ-max ℓ' ℓ''))) [ (LiftHoms C ℓ'' [ c ,-]) + , LiftF {ℓ''}{ℓ'} ∘F (F ∘F lowerHoms C ℓ'') ]) + Iso⟨ yoneda (LiftF {ℓ''}{ℓ'} ∘F (F ∘F lowerHoms C ℓ'')) c ⟩ + Lift {ℓ''}{ℓ'} (fst (F ⟅ c ⟆)) + Iso⟨ invIso LiftIso ⟩ + (fst (F ⟅ c ⟆)) ∎Iso where + + the-iso : Iso ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) + [ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-]) + , LiftF {ℓ''}{ℓ'} ∘F F ]) + ((FUNCTOR (LiftHoms C ℓ'') (SET (ℓ-max ℓ' ℓ''))) + [ (LiftHoms C ℓ'' [ c ,-]) + , LiftF {ℓ''}{ℓ'} ∘F (F ∘F lowerHoms C ℓ'') ]) + the-iso .fun α .N-ob d f = α .N-ob d f + the-iso .fun α .N-hom g = α .N-hom (g .lower) + the-iso .inv β .N-ob d f = β .N-ob d f + the-iso .inv β .N-hom g = β .N-hom (lift g) + the-iso .rightInv β = refl + the-iso .leftInv α = refl + +yonedaᴾ* : {C : Category ℓ ℓ'}(F : Functor (C ^op) (SET ℓ'')) + → (c : Category.ob C) + → Iso (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) + [ LiftF {ℓ'}{ℓ''} ∘F (C [-, c ]) + , LiftF {ℓ''}{ℓ'} ∘F F ]) + (fst (F ⟅ c ⟆)) +yonedaᴾ* {ℓ}{ℓ'}{ℓ''}{C} F c = + (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) + [ LiftF {ℓ'}{ℓ''} ∘F (C [-, c ]) , LiftF {ℓ''}{ℓ'} ∘F F ]) Iso⟨ the-iso ⟩ + (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) + [ LiftF {ℓ'}{ℓ''} ∘F ((C ^op) [ c ,-]) + , LiftF {ℓ''}{ℓ'} ∘F F ]) Iso⟨ yoneda* F c ⟩ + fst (F ⟅ c ⟆) ∎Iso where + + the-iso : + Iso (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) + [ LiftF {ℓ'}{ℓ''} ∘F (C [-, c ]) , LiftF {ℓ''}{ℓ'} ∘F F ]) + (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ'')) + [ LiftF {ℓ'}{ℓ''} ∘F ((C ^op) [ c ,-]) , LiftF {ℓ''}{ℓ'} ∘F F ]) + the-iso .fun α .N-ob = α .N-ob + the-iso .fun α .N-hom = α .N-hom + the-iso .inv β .N-ob = β .N-ob + the-iso .inv β .N-hom = β .N-hom + the-iso .rightInv = λ b → refl + the-iso .leftInv = λ a → refl + -- Yoneda embedding -- TODO: probably want to rename/refactor module _ {C : Category ℓ ℓ} where @@ -179,4 +267,5 @@ module _ {C : Category ℓ ℓ} where (yo-yo-yo _ (p i)) isFullyFaithfulYO : isFullyFaithful YO - isFullyFaithfulYO = isFull+Faithful→isFullyFaithful {F = YO} isFullYO isFaithfulYO + isFullyFaithfulYO = + isFull+Faithful→isFullyFaithful {F = YO} isFullYO isFaithfulYO diff --git a/Cubical/Data/Graph/Base.agda b/Cubical/Data/Graph/Base.agda index 5cb7797f6c..f79ed07e85 100644 --- a/Cubical/Data/Graph/Base.agda +++ b/Cubical/Data/Graph/Base.agda @@ -33,6 +33,28 @@ record GraphHom (G : Graph ℓv ℓe ) (G' : Graph ℓv' ℓe') open GraphHom public +module _ {ℓv ℓe ℓv' ℓe' ℓv'' ℓe''} + {G : Graph ℓv ℓe}{G' : Graph ℓv' ℓe'}{G'' : Graph ℓv'' ℓe''} where + _⋆GrHom_ : GraphHom G G' → GraphHom G' G'' → GraphHom G G'' + (ϕ ⋆GrHom ψ) ._$g_ = λ z → ψ $g (ϕ $g z) + (ϕ ⋆GrHom ψ) ._<$g>_ e = ψ <$g> (ϕ <$g> e) + + _∘GrHom_ : GraphHom G' G'' → GraphHom G G' → GraphHom G G'' + ψ ∘GrHom ϕ = ϕ ⋆GrHom ψ + +IdHom : ∀ {ℓv ℓe} {G : Graph ℓv ℓe} → GraphHom G G +IdHom {G} ._$g_ = λ z → z +IdHom {G} ._<$g>_ = λ z → z + +GrHom≡ : ∀ {ℓg ℓg' ℓh ℓh'} + {G : Graph ℓg ℓg'}{H : Graph ℓh ℓh'} {ϕ ψ : GraphHom G H} + → (h : ∀ v → ϕ $g v ≡ ψ $g v) + → (∀ {v w} (e : G .Edge v w) + → PathP (λ i → H .Edge (h v i) (h w i)) (ϕ <$g> e) (ψ <$g> e)) + → ϕ ≡ ψ +GrHom≡ h k i $g x = h x i +GrHom≡ h k i <$g> x = k x i + GraphGr : ∀ ℓv ℓe → Graph _ _ Node (GraphGr ℓv ℓe) = Graph ℓv ℓe Edge (GraphGr ℓv ℓe) G G' = GraphHom G G' @@ -46,7 +68,8 @@ record DiagMor {G : Graph ℓv ℓe} (F : Diag ℓd G) (F' : Diag ℓd' G) : Type (ℓ-suc (ℓ-max (ℓ-max ℓv ℓe) (ℓ-suc (ℓ-max ℓd ℓd')))) where field nat : ∀ (x : Node G) → F $g x → F' $g x - comSq : ∀ {x y : Node G} (f : Edge G x y) → nat y ∘ F <$g> f ≡ F' <$g> f ∘ nat x + comSq : ∀ {x y : Node G} (f : Edge G x y) + → nat y ∘ F <$g> f ≡ F' <$g> f ∘ nat x open DiagMor public diff --git a/Cubical/Tactics/CategorySolver/Examples.agda b/Cubical/Tactics/CategorySolver/Examples.agda new file mode 100644 index 0000000000..05a5c8d958 --- /dev/null +++ b/Cubical/Tactics/CategorySolver/Examples.agda @@ -0,0 +1,46 @@ +{-# OPTIONS --safe #-} + +{- + The Category Solver solveCat! solves equations in a category that + hold up to associativity and unit laws + + This file shows some examples of how to use it. +-} + +module Cubical.Tactics.CategorySolver.Examples where + +open import Cubical.Foundations.Prelude + +open import Cubical.Categories.Category +open import Cubical.Tactics.CategorySolver.Reflection + +private + variable + ℓ ℓ' : Level + +module Examples (𝓒 : Category ℓ ℓ') where + open Category 𝓒 + + _ : ∀ {A} → id {A} ≡ id {A} + _ = solveCat! 𝓒 + + _ : ∀ {A B}{f : 𝓒 [ A , B ]} + → f ∘ id ≡ f + _ = solveCat! 𝓒 + + _ : ∀ {A B}{f : 𝓒 [ A , B ]} + → id ∘ (id ∘ id ∘ f) ∘ id ≡ id ∘ id ∘ (id ∘ f) + _ = solveCat! 𝓒 + + _ : ∀ {A B C}{f : 𝓒 [ A , B ]}{g : 𝓒 [ B , C ]} + → f ⋆ g ≡ g ∘ (id ∘ f) ∘⟨ 𝓒 ⟩ id + _ = solveCat! 𝓒 + + ex : ∀ {A B C}(f : 𝓒 [ A , B ])(g : 𝓒 [ B , C ])(h : 𝓒 [ A , C ]) + → (f ⋆ (id ⋆ g)) ≡ h + → f ⋆ g ≡ h ⋆ id + ex f g h p = + f ⋆ g ≡⟨ solveCat! 𝓒 ⟩ + (f ⋆ (id ⋆ g)) ≡⟨ p ⟩ + h ≡⟨ solveCat! 𝓒 ⟩ + h ⋆ id ∎ diff --git a/Cubical/Tactics/CategorySolver/Reflection.agda b/Cubical/Tactics/CategorySolver/Reflection.agda new file mode 100644 index 0000000000..4f6ff5d596 --- /dev/null +++ b/Cubical/Tactics/CategorySolver/Reflection.agda @@ -0,0 +1,61 @@ +{-# OPTIONS --safe #-} + +module Cubical.Tactics.CategorySolver.Reflection where + +open import Cubical.Foundations.Prelude + +open import Agda.Builtin.Reflection hiding (Type) +open import Agda.Builtin.String + +open import Cubical.Data.Bool +open import Cubical.Data.List +open import Cubical.Data.Maybe +open import Cubical.Data.Sigma +open import Cubical.Data.Unit +open import Cubical.Reflection.Base + +open import Cubical.Tactics.CategorySolver.Solver +open import Cubical.Tactics.Reflection + +open import Cubical.Categories.Category +open import Cubical.Categories.Constructions.Free.Category.Base + +private + variable + ℓ ℓ' : Level + +module ReflectionSolver where + module _ (category : Term) where + pattern category-args xs = + _ h∷ _ h∷ _ v∷ xs + + pattern “id” = + def (quote Category.id) (category-args (_ h∷ [])) + + pattern “⋆” f g = + def (quote Category._⋆_) (category-args (_ h∷ _ h∷ _ h∷ f v∷ g v∷ [])) + + -- Parse the input into an exp + buildExpression : Term → Term + buildExpression “id” = con (quote FreeCategory.idₑ) [] + buildExpression (“⋆” f g) = + con (quote FreeCategory._⋆ₑ_) + (buildExpression f v∷ buildExpression g v∷ []) + buildExpression f = con (quote FreeCategory.↑_) (f v∷ []) + + solve-macro : Term -- ^ The term denoting the category + → Term -- ^ The hole whose goal should be an equality between + -- morphisms in the category + → TC Unit + solve-macro category = + equation-solver (quote Category.id ∷ quote Category._⋆_ ∷ []) mk-call true + where + mk-call : Term → Term → TC Term + mk-call lhs rhs = returnTC (def (quote solve) + (category v∷ + buildExpression category lhs v∷ + buildExpression category rhs v∷ + def (quote refl) [] v∷ [])) +macro + solveCat! : Term → Term → TC _ + solveCat! = ReflectionSolver.solve-macro diff --git a/Cubical/Tactics/CategorySolver/Solver.agda b/Cubical/Tactics/CategorySolver/Solver.agda new file mode 100644 index 0000000000..a79b713f32 --- /dev/null +++ b/Cubical/Tactics/CategorySolver/Solver.agda @@ -0,0 +1,57 @@ +{-# 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 + -- Semantics in 𝓒 itself, tautologically + open FreeCategory (Cat→Graph 𝓒) + sem𝓒 = ε {𝓒 = 𝓒} + ⟦_⟧c = sem𝓒 .F-hom + 𝓟 = PowerCategory (𝓒 .ob) (SET (ℓ-max ℓ ℓ')) + 𝓘 : Functor FreeCat 𝓟 + 𝓘 = PseudoYoneda {C = FreeCat} + + -- Semantics in 𝓟 (𝓒 .ob), interpreting fun symbols using Yoneda + module YoSem = Semantics 𝓟 (𝓘 ∘Interp η) + ⟦_⟧yo = YoSem.sem .F-hom + + -- | Evaluate by taking the semantics in 𝓟 (𝓒 .ob) + eval : ∀ {A B} → FreeCat [ A , B ] → _ + eval {A}{B} e = ⟦ e ⟧yo + + -- Evaluation agrees with the Yoneda embedding, and so is fully faithful + Yo-YoSem-agree : 𝓘 ≡ YoSem.sem + Yo-YoSem-agree = YoSem.sem-uniq refl + + -- If two expressions in the free category are equal when evaluated + -- in 𝓟 (𝓒 .ob), then they are equal, and so are equal when + -- evaluated in 𝓒. + 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 diff --git a/Cubical/Tactics/FunctorSolver/Examples.agda b/Cubical/Tactics/FunctorSolver/Examples.agda new file mode 100644 index 0000000000..26c785e9f4 --- /dev/null +++ b/Cubical/Tactics/FunctorSolver/Examples.agda @@ -0,0 +1,45 @@ +{-# OPTIONS --safe #-} + +{- + The functor solver solveFunctor! C D F solves equations in a + category D that hold up to associativity/unit in D as well as + Functoriality of the functor F. + + This file shows some examples of how to use it. +-} + +module Cubical.Tactics.FunctorSolver.Examples where + +open import Cubical.Foundations.Prelude + +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Tactics.FunctorSolver.Reflection + +private + variable + ℓ ℓ' : Level + C D : Category ℓ ℓ' + F : Functor C D + +module Examples (F : Functor C D) where + open Category + open Functor + + _ : ∀ {A B}{f : D [ A , B ]} + → D .id ∘⟨ D ⟩ f ≡ f ∘⟨ D ⟩ D .id + _ = solveFunctor! C D F + + _ : ∀ {A} + → D .id ≡ F ⟪ (C .id {A}) ⟫ + _ = solveFunctor! C D F + + + _ : {W X Y : C .ob} + → {Z : D .ob} + → {f : C [ W , X ]} + → {g : C [ X , Y ]} + → {h : D [ F ⟅ Y ⟆ , Z ]} + → h ∘⟨ D ⟩ F ⟪ (g ∘⟨ C ⟩ C .id) ∘⟨ C ⟩ f ⟫ ∘⟨ D ⟩ F ⟪ C .id ⟫ + ≡ D .id ∘⟨ D ⟩ h ∘⟨ D ⟩ F ⟪ C .id ∘⟨ C ⟩ g ⟫ ∘⟨ D ⟩ F ⟪ f ⟫ + _ = solveFunctor! C D F diff --git a/Cubical/Tactics/FunctorSolver/Reflection.agda b/Cubical/Tactics/FunctorSolver/Reflection.agda new file mode 100644 index 0000000000..9faaca98e6 --- /dev/null +++ b/Cubical/Tactics/FunctorSolver/Reflection.agda @@ -0,0 +1,95 @@ +{-# OPTIONS --safe #-} + +module Cubical.Tactics.FunctorSolver.Reflection where + +open import Cubical.Foundations.Prelude + +open import Agda.Builtin.Reflection hiding (Type) +open import Agda.Builtin.String + +open import Cubical.Data.Bool +open import Cubical.Data.List +open import Cubical.Data.Maybe +open import Cubical.Data.Sigma +open import Cubical.Data.Unit + +open import Cubical.Reflection.Base +open import Cubical.Tactics.FunctorSolver.Solver +open import Cubical.Tactics.Reflection + +open import Cubical.Categories.Category +open import Cubical.Categories.Constructions.Free.Category +open import Cubical.Categories.Constructions.Free.Functor +open import Cubical.Categories.Functor + +private + variable + ℓ ℓ' : Level + +module ReflectionSolver where + module _ (domain : Term) (codomain : Term) (functor : Term) where + -- the two implicit levels and the category + pattern category-args xs = + _ h∷ _ h∷ _ v∷ xs + + -- the four implicit levels, the two implicit categories and the functor + pattern functor-args functor xs = + _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ functor v∷ xs + + pattern “id” = + def (quote Category.id) (category-args (_ h∷ [])) + + pattern “⋆” f g = + def (quote Category._⋆_) (category-args (_ h∷ _ h∷ _ h∷ f v∷ g v∷ [])) + + pattern “F” functor f = + def (quote Functor.F-hom) (functor-args functor (_ h∷ _ h∷ f v∷ [])) + + -- Parse the input into an exp + buildDomExpression : Term → Term + buildDomExpression “id” = con (quote FreeCategory.idₑ) [] + buildDomExpression (“⋆” f g) = + con (quote FreeCategory._⋆ₑ_) + (buildDomExpression f v∷ buildDomExpression g v∷ []) + buildDomExpression f = con (quote FreeCategory.↑_) (f v∷ []) + + buildCodExpression : Term → TC Term + buildCodExpression “id” = returnTC (con (quote FreeFunctor.idₑ) []) + buildCodExpression (“⋆” f g) = + ((λ fe ge → (con (quote FreeFunctor._⋆ₑ_) (fe v∷ ge v∷ []))) + <$> buildCodExpression f) + <*> buildCodExpression g + buildCodExpression (“F” functor' f) = do + unify functor functor' + returnTC (con (quote FreeFunctor.F⟪_⟫) (buildDomExpression f v∷ [])) + buildCodExpression f = returnTC (con (quote FreeFunctor.↑_) (f v∷ [])) + + solve-macro : Bool -- ^ whether to give the more detailed but messier error + -- message on failure + → Term -- ^ The term denoting the domain category + → Term -- ^ The term denoting the codomain category + → Term -- ^ The term denoting the functor + → Term -- ^ The hole whose goal should be an equality between + -- morphisms in the codomain category + → TC Unit + solve-macro b dom cod fctor = + equation-solver + (quote Category.id ∷ quote Category._⋆_ ∷ quote Functor.F-hom ∷ []) + mk-call + b + where + + mk-call : Term → Term → TC Term + mk-call lhs rhs = do + l-e ← buildCodExpression dom cod fctor lhs + r-e ← buildCodExpression dom cod fctor rhs + -- unify l-e r-e + returnTC (def (quote Eval.solve) ( + dom v∷ cod v∷ fctor v∷ + l-e v∷ r-e v∷ def (quote refl) [] v∷ [])) +macro + solveFunctor! : Term → Term → Term → Term → TC _ + solveFunctor! = ReflectionSolver.solve-macro false + + solveFunctorDebug! : Term → Term → Term → Term → TC _ + solveFunctorDebug! = ReflectionSolver.solve-macro true diff --git a/Cubical/Tactics/FunctorSolver/Solver.agda b/Cubical/Tactics/FunctorSolver/Solver.agda new file mode 100644 index 0000000000..aee48d7fe7 --- /dev/null +++ b/Cubical/Tactics/FunctorSolver/Solver.agda @@ -0,0 +1,66 @@ +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Tactics.FunctorSolver.Solver where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Path + +open import Cubical.Data.Graph.Base +open import Cubical.Data.Equality renaming (refl to reflEq) + hiding (_∙_; sym; transport) + +open import Cubical.Categories.Category +open import Cubical.Categories.Constructions.Free.Functor +open import Cubical.Categories.Constructions.Power +open import Cubical.Categories.Functor renaming (Id to IdF) +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.UnderlyingGraph + +private + variable + ℓc ℓc' ℓd ℓd' ℓb ℓb' : Level +open Category +open Functor +open NatIso +open NatTrans + +module Eval (𝓒 : Category ℓc ℓc') (𝓓 : Category ℓd ℓd') (𝓕 : Functor 𝓒 𝓓) where + open FreeFunctor (Cat→Graph 𝓒) (Cat→Graph 𝓓) (𝓕 .F-ob) + + Free𝓒 = FG + η𝓒 = ηG + Free𝓓 = FH + η𝓓 = ηH + Free𝓕 = Fϕ + 𝓟 = PowerCategory (Free𝓓 .ob) (SET (ℓ-max (ℓ-max (ℓ-max ℓc ℓc') ℓd) ℓd')) + PsYo : Functor Free𝓓 𝓟 + PsYo = PseudoYoneda {C = Free𝓓} + + module TautoSem = Semantics {𝓒 = 𝓒} {𝓓 = 𝓓} {𝓕 = 𝓕} IdHom IdHom reflEq + module YoSem = Semantics {𝓒 = 𝓟} {𝓓 = 𝓟} {𝓕 = IdF} + (Functor→GraphHom (PsYo ∘F Free𝓕) ∘GrHom η𝓒) + (Functor→GraphHom PsYo ∘GrHom η𝓓) + reflEq + + Yo-YoSem-Agree : Path _ PsYo YoSem.semH + Yo-YoSem-Agree = sem-uniq-H where + open YoSem.Uniqueness (PsYo ∘F Free𝓕) PsYo F-rUnit refl refl + (compPath→Square (sym (lUnit (eqToPath reflEq)) + ∙ rUnit refl)) + solve : ∀ {A B} + → (e e' : Free𝓓 [ A , B ]) + → (p : Path _ (YoSem.semH ⟪ e ⟫) (YoSem.semH ⟪ e' ⟫)) + → Path _ (TautoSem.semH ⟪ e ⟫) (TautoSem.semH ⟪ e' ⟫) + solve {A}{B} e e' p = + cong (TautoSem.semH .F-hom) (isFaithfulPseudoYoneda _ _ _ _ lem) where + lem : Path _ (PsYo ⟪ e ⟫) (PsYo ⟪ e' ⟫) + lem = transport + (λ i → Path _ + (Yo-YoSem-Agree (~ i) ⟪ e ⟫) + (Yo-YoSem-Agree (~ i) ⟪ e' ⟫)) + p + +solve = Eval.solve diff --git a/Cubical/Tactics/Reflection.agda b/Cubical/Tactics/Reflection.agda new file mode 100644 index 0000000000..9db131d08c --- /dev/null +++ b/Cubical/Tactics/Reflection.agda @@ -0,0 +1,114 @@ +-- SPDX-License-Identifier: BSD-3-Clause +{-# OPTIONS --safe #-} +module Cubical.Tactics.Reflection where + +{- Utilities common to different reflection solvers. + + Most of these are copied/adapted from the 1Lab +-} + +open import Cubical.Foundations.Prelude + +open import Agda.Builtin.Reflection hiding (Type) + +open import Cubical.Data.Bool +open import Cubical.Data.List +open import Cubical.Data.Maybe +open import Cubical.Data.Sigma +open import Cubical.Data.Unit + +open import Cubical.Reflection.Base + +private + variable + ℓ ℓ' : Level + +_<$>_ : ∀ {ℓ ℓ'} {A : Type ℓ}{B : Type ℓ'} → (A → B) → TC A → TC B +f <$> t = t >>= λ x → returnTC (f x) + +_<*>_ : ∀ {ℓ ℓ'} {A : Type ℓ}{B : Type ℓ'} → TC (A → B) → TC A → TC B +s <*> t = s >>= λ f → t >>= λ x → returnTC (f x) + +wait-for-args : List (Arg Term) → TC (List (Arg Term)) +wait-for-type : Term → TC Term + +wait-for-type (var x args) = var x <$> wait-for-args args +wait-for-type (con c args) = con c <$> wait-for-args args +wait-for-type (def f args) = def f <$> wait-for-args args +wait-for-type (lam v (abs x t)) = returnTC (lam v (abs x t)) +wait-for-type (pat-lam cs args) = returnTC (pat-lam cs args) +wait-for-type (pi (arg i a) (abs x b)) = do + a ← wait-for-type a + b ← wait-for-type b + returnTC (pi (arg i a) (abs x b)) +wait-for-type (agda-sort s) = returnTC (agda-sort s) +wait-for-type (lit l) = returnTC (lit l) +wait-for-type (meta x x₁) = blockOnMeta x +wait-for-type unknown = returnTC unknown + +wait-for-args [] = returnTC [] +wait-for-args (arg i a ∷ xs) = + (_∷_ <$> (arg i <$> wait-for-type a)) <*> wait-for-args xs + +unapply-path : Term → TC (Maybe (Term × Term × Term)) +unapply-path red@(def (quote PathP) (l h∷ T v∷ x v∷ y v∷ [])) = do + domain ← newMeta (def (quote Type) (l v∷ [])) + ty ← returnTC (def (quote Path) (domain v∷ x v∷ y v∷ [])) + debugPrint "tactic" 50 + (strErr "(no reduction) unapply-path: got a " ∷ termErr red + ∷ strErr " but I really want it to be " ∷ termErr ty ∷ []) + unify red ty + returnTC (just (domain , x , y)) +unapply-path tm = reduce tm >>= λ where + tm@(meta _ _) → do + dom ← newMeta (def (quote Type) []) + l ← newMeta dom + r ← newMeta dom + unify tm (def (quote Type) (varg dom ∷ varg l ∷ varg r ∷ [])) + wait-for-type l + wait-for-type r + returnTC (just (dom , l , r)) + red@(def (quote PathP) (l h∷ T v∷ x v∷ y v∷ [])) → do + domain ← newMeta (def (quote Type) (l v∷ [])) + ty ← returnTC (def (quote Path) (domain v∷ x v∷ y v∷ [])) + debugPrint "tactic" 50 + (strErr "unapply-path: got a " ∷ termErr red + ∷ strErr " but I really want it to be " ∷ termErr ty ∷ []) + unify red ty + returnTC (just (domain , x , y)) + _ → returnTC nothing + +{- + get-boundary maps a term 'x ≡ y' to the pair '(x,y)' +-} +get-boundary : Term → TC (Maybe (Term × Term)) +get-boundary tm = unapply-path tm >>= λ where + (just (_ , x , y)) → returnTC (just (x , y)) + nothing → returnTC nothing + +equation-solver : List Name → (Term -> Term -> TC Term) → Bool → Term → TC Unit +equation-solver don't-Reduce mk-call debug hole = + withNormalisation false ( + dontReduceDefs don't-Reduce ( + do + -- | First we normalize the goal + goal ← inferType hole >>= reduce + -- | Then we parse the goal into an AST + just (lhs , rhs) ← get-boundary goal + where + nothing + → typeError(strErr "The functor solver failed to parse the goal" + ∷ termErr goal ∷ []) + -- | Then we invoke the solver + -- | And we unify the result of the solver with the original hole. + elhs ← normalise lhs + erhs ← normalise rhs + call ← mk-call elhs erhs + let unify-with-goal = (unify hole call) + noConstraints ( + if debug + then unify-with-goal + else ( + unify-with-goal <|> + typeError ((strErr "Could not equate the following expressions:\n " + ∷ termErr elhs ∷ strErr "\nAnd\n " ∷ termErr erhs ∷ []))))))