From d7a0db1a2f2ca237f4257d1bef1c8f4a384e12b3 Mon Sep 17 00:00:00 2001 From: "Max S. New" Date: Fri, 14 Jul 2023 11:41:21 -0400 Subject: [PATCH] update to cubical HEAD (#39) --- Cubical/Categories/Adjoint/2Var.agda | 16 +- .../Categories/Adjoint/UniversalElements.agda | 4 +- Cubical/Categories/Bifunctor/Redundant.agda | 6 + .../BinProduct/AsLeftAdjoint.agda | 164 --- .../BinProduct/Redundant/Assoc.agda | 3 +- .../BinProduct/Redundant/Assoc/ToLeft.agda | 3 +- .../BinProduct/Redundant/Assoc/ToRight.agda | 3 +- .../BinProduct/Redundant/Base.agda | 3 +- .../Constructions/Elements/More.agda | 37 - .../{Category.agda => Category/Quiver.agda} | 2 +- .../Constructions/Free/Functor.agda | 344 ------- .../Free/Functor/Uniqueness.agda | 210 ---- .../Constructions/Free/General.agda | 157 --- .../Constructions/Free/UnderlyingGraph.agda | 262 ----- Cubical/Categories/Constructions/Lift.agda | 37 - Cubical/Categories/Constructions/Power.agda | 29 - .../Categories/Constructions/Presented.agda | 2 +- .../Constructions/Product/More.agda | 30 - Cubical/Categories/Exponentials.agda | 9 +- .../Categories/Instances/Functors/More.agda | 18 - Cubical/Categories/Instances/Sets/More.agda | 26 +- .../Categories/Limits/BinProduct/More.agda | 92 +- Cubical/Categories/Limits/Terminal/More.agda | 7 - Cubical/Categories/Monad/Algebra.agda | 24 +- Cubical/Categories/Monad/ExtensionSystem.agda | 16 +- .../NaturalTransformation/More.agda | 47 +- Cubical/Categories/Presheaf/More.agda | 64 +- Cubical/Categories/Presheaf/Morphism.agda | 93 -- .../Categories/Presheaf/Representable.agda | 296 ------ .../Categories/Profunctor/Equivalence.agda | 647 ++++++------ Cubical/Categories/Profunctor/General.agda | 935 +++++++++--------- Cubical/Categories/Yoneda/More.agda | 81 -- Cubical/Data/Graph/Properties.agda | 32 - Cubical/Foundations/Isomorphism/More.agda | 22 + Cubical/Tactics/CategorySolver/Examples.agda | 35 - .../Tactics/CategorySolver/Reflection.agda | 71 -- Cubical/Tactics/CategorySolver/Solver.agda | 54 - Cubical/Tactics/FunctorSolver/Examples.agda | 36 - Cubical/Tactics/FunctorSolver/Reflection.agda | 90 -- Cubical/Tactics/FunctorSolver/Solver.agda | 68 -- Cubical/Tactics/Reflection.agda | 116 --- Makefile | 2 +- 42 files changed, 997 insertions(+), 3196 deletions(-) delete mode 100644 Cubical/Categories/Constructions/BinProduct/AsLeftAdjoint.agda delete mode 100644 Cubical/Categories/Constructions/Elements/More.agda rename Cubical/Categories/Constructions/Free/{Category.agda => Category/Quiver.agda} (98%) delete mode 100644 Cubical/Categories/Constructions/Free/Functor.agda delete mode 100644 Cubical/Categories/Constructions/Free/Functor/Uniqueness.agda delete mode 100644 Cubical/Categories/Constructions/Free/General.agda delete mode 100644 Cubical/Categories/Constructions/Free/UnderlyingGraph.agda delete mode 100644 Cubical/Categories/Constructions/Lift.agda delete mode 100644 Cubical/Categories/Constructions/Power.agda delete mode 100644 Cubical/Categories/Constructions/Product/More.agda delete mode 100644 Cubical/Categories/Presheaf/Morphism.agda delete mode 100644 Cubical/Categories/Presheaf/Representable.agda delete mode 100644 Cubical/Data/Graph/Properties.agda create mode 100644 Cubical/Foundations/Isomorphism/More.agda delete mode 100644 Cubical/Tactics/CategorySolver/Examples.agda delete mode 100644 Cubical/Tactics/CategorySolver/Reflection.agda delete mode 100644 Cubical/Tactics/CategorySolver/Solver.agda delete mode 100644 Cubical/Tactics/FunctorSolver/Examples.agda delete mode 100644 Cubical/Tactics/FunctorSolver/Reflection.agda delete mode 100644 Cubical/Tactics/FunctorSolver/Solver.agda delete mode 100644 Cubical/Tactics/Reflection.agda diff --git a/Cubical/Categories/Adjoint/2Var.agda b/Cubical/Categories/Adjoint/2Var.agda index 2400bdcc..fae0262c 100644 --- a/Cubical/Categories/Adjoint/2Var.agda +++ b/Cubical/Categories/Adjoint/2Var.agda @@ -32,17 +32,17 @@ open Category (E : Category ℓE ℓE') (F : Bifunctor C D E) → Type _ 2VarRightAdjointR C D E F = - ParamUnivElt ((C ^op) ×C E) D - (ForgetPar (assoc-bif (HomBif E ∘Fl - (rec D C (Sym F) ^opF) ∘F - ×-op-commute⁻ {C = D}{D = C}))) + UniversalElements ((C ^op) ×C E) D + (assoc-bif (HomBif E ∘Fl + (rec D C (Sym F) ^opF) ∘F + ×-op-commute⁻ {C = D}{D = C})) 2VarRightAdjointL : (C : Category ℓC ℓC') (D : Category ℓD ℓD') (E : Category ℓE ℓE') (F : Bifunctor C D E) → Type _ 2VarRightAdjointL C D E F = - ParamUnivElt ((D ^op) ×C E) C - (ForgetPar (assoc-bif (HomBif E ∘Fl - (rec C D F ^opF) ∘F - ×-op-commute⁻ {C = C}{D = D}))) + UniversalElements ((D ^op) ×C E) C + (assoc-bif (HomBif E ∘Fl + (rec C D F ^opF) ∘F + ×-op-commute⁻ {C = C}{D = D})) diff --git a/Cubical/Categories/Adjoint/UniversalElements.agda b/Cubical/Categories/Adjoint/UniversalElements.agda index 4295043f..61c179e9 100644 --- a/Cubical/Categories/Adjoint/UniversalElements.agda +++ b/Cubical/Categories/Adjoint/UniversalElements.agda @@ -16,13 +16,13 @@ open Category RightAdjoint : (C : Category ℓC ℓC') (D : Category ℓD ℓD') (F : Functor C D) → Type _ -RightAdjoint C D F = ParamUnivElt D C (Functor→Profo-* C D F) +RightAdjoint C D F = UniversalElements D C (Functor→Profo-* C D F) RightAdjointAt : (C : Category ℓC ℓC') (D : Category ℓD ℓD') (F : Functor C D) (d : D .ob) → Type _ -RightAdjointAt C D F = RepresentableAt D C (Functor→Profo-* C D F) +RightAdjointAt C D F = UniversalElementAt D C (Functor→Profo-* C D F) LeftAdjoint : (C : Category ℓC ℓC') (D : Category ℓD ℓD') diff --git a/Cubical/Categories/Bifunctor/Redundant.agda b/Cubical/Categories/Bifunctor/Redundant.agda index 8d88ca86..7c21d41b 100644 --- a/Cubical/Categories/Bifunctor/Redundant.agda +++ b/Cubical/Categories/Bifunctor/Redundant.agda @@ -461,6 +461,12 @@ HomBif C = mkBifunctorSep Hom where Hom .Bif-R-seq f' f'' = funExt λ f → sym (C .⋆Assoc f f' f'') Hom .SepBif-RL-commute f g = funExt (λ h → sym (C .⋆Assoc f h g)) +BifunctorToParFunctor : Bifunctor C D E → Functor (C ×C D) E +BifunctorToParFunctor F .F-ob (c , d) = F .Bif-ob c d +BifunctorToParFunctor F .F-hom (f , g) = F .Bif-hom× f g +BifunctorToParFunctor F .F-id = F .Bif-×-id +BifunctorToParFunctor F .F-seq f g = F .Bif-×-seq _ _ _ _ + open Separate.Bifunctor ForgetPar : Bifunctor C D E → Separate.Bifunctor C D E ForgetPar F .Bif-ob = F .Bif-ob diff --git a/Cubical/Categories/Constructions/BinProduct/AsLeftAdjoint.agda b/Cubical/Categories/Constructions/BinProduct/AsLeftAdjoint.agda deleted file mode 100644 index a49ac555..00000000 --- a/Cubical/Categories/Constructions/BinProduct/AsLeftAdjoint.agda +++ /dev/null @@ -1,164 +0,0 @@ --- TODO: Better Name? --- The cartesian product of categories, but presented by the universal property --- that is is left adjoint to forming functor categories --- --- C ×C D → E ≅ C → FUNCTOR D E -{-# OPTIONS --safe #-} - -module Cubical.Categories.Constructions.BinProduct.AsLeftAdjoint where - -open import Cubical.Foundations.Prelude -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor.Base hiding (Id) -open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧) -open import Cubical.Data.Graph.Base -open import Cubical.Data.Sum as Sum -open import Cubical.Data.Sigma - -import Cubical.Categories.Constructions.BinProduct as BP -open import Cubical.Categories.Constructions.Free.Category as Free -open import Cubical.Categories.Constructions.Presented as Presented -open import Cubical.Categories.Bifunctor - hiding (Bifunctor→Functor; UniversalBifunctor) - -private - variable - ℓc ℓc' ℓd ℓd' : Level - -open Category -open Functor -open Quiver -open Interp -open Axioms - - -module _ (C : Category ℓc ℓc') (D : Category ℓd ℓd') where - data ProdGenerator : Type (ℓ-max (ℓ-max ℓc ℓc') (ℓ-max ℓd ℓd')) where - _id×_ : ∀ (c : C .ob) {d d' : D .ob} (g : D [ d , d' ]) → ProdGenerator - _×id_ : ∀ {c c' : C .ob} (f : C [ c , c' ]) (d : D .ob) → ProdGenerator - _×ₑ_ : ∀ {c c' : C .ob}{d d' : D .ob} - (f : C [ c , c' ]) (g : D [ d , d' ]) → ProdGenerator - - data ProdAx : Type (ℓ-max (ℓ-max ℓc ℓc') (ℓ-max ℓd ℓd')) where - combine-id×id : ∀ {c c' d d'} (f : C [ c , c' ])(g : D [ d , d' ]) - → ProdAx - combine-×id× : ∀ {c c' d d'} (f : C [ c , c' ])(g : D [ d , d' ]) - → ProdAx - id×-Id : ∀ (c : C .ob) (d : D .ob) → ProdAx - id×-Comp : ∀ (c : C .ob) {d d' d'' : D .ob} - (g' : D [ d' , d'' ])(g : D [ d , d' ]) - → ProdAx - ×id-Id : ∀ (c : C .ob) (d : D .ob) → ProdAx - ×id-Comp : ∀ {c c' c'' : C .ob} - (f' : C [ c' , c'' ])(f : C [ c , c' ]) - (d : D .ob) - → ProdAx - - private - Q : Quiver _ _ - Q .ob = C .ob × D .ob - Q .mor = ProdGenerator - Q .dom (_×ₑ_ {c = c}{d = d} _ _) = c , d - Q .cod (_×ₑ_ {c' = c'}{d' = d'} _ _) = c' , d' - Q .dom (_id×_ c {d = d} g) = c , d - Q .cod (_id×_ c {d' = d'} g) = c , d' - Q .dom (_×id_ {c = c} f d) = c , d - Q .cod (_×id_ {c' = c'} f d) = c' , d - - Ax : Axioms Q _ - Ax = mkAx Q ProdAx λ - { (combine-id×id {c = c}{c' = c'}{d = d}{d' = d'} f g) → _ , _ , - η Q .I-hom (c' id× g) ∘⟨ FreeCat Q ⟩ η Q .I-hom (f ×id d) - , η Q .I-hom (f ×ₑ g) - ; (combine-×id× {c = c}{c' = c'}{d = d}{d' = d'} f g) → _ , _ , - η Q .I-hom (f ×id d') ∘⟨ FreeCat Q ⟩ η Q .I-hom (c id× g) - , η Q .I-hom (f ×ₑ g) - ; (id×-Id c d) → _ , _ , - (η Q .I-hom (c id× D .id {d})) - , (FreeCat Q .id) - ; (id×-Comp c g' g) → _ , _ , - η Q .I-hom (c id× (g' ∘⟨ D ⟩ g)) - , η Q .I-hom (c id× g') ∘⟨ FreeCat Q ⟩ η Q .I-hom (c id× g) - ; (×id-Id c d) → _ , _ , - η Q .I-hom ((C .id {c}) ×id d) - , FreeCat Q .id - ; (×id-Comp f' f d) → _ , _ , - η Q .I-hom ((f' ∘⟨ C ⟩ f) ×id d) - , η Q .I-hom (f' ×id d) ∘⟨ FreeCat Q ⟩ η Q .I-hom (f ×id d) - } - - _×C_ : Category _ _ - _×C_ = PresentedCat Q Ax - - open Bifunctor - ×l : (c : C .ob) → Functor D _×C_ - ×l c .F-ob d = c , d - ×l c .F-hom g = ηP Q Ax .I-hom (c id× g) - ×l c .F-id {d} = ηEq Q Ax (id×-Id c d) - ×l c .F-seq g g' = ηEq Q Ax (id×-Comp c g' g) - - ×r : (d : D .ob) → Functor C _×C_ - ×r d .F-ob c = c , d - ×r d .F-hom f = ηP Q Ax .I-hom (f ×id d) - ×r d .F-id {c} = ηEq Q Ax (×id-Id c d) - ×r d .F-seq f f' = ηEq Q Ax (×id-Comp f' f d) - - ×lr : ∀ {c c' d d'}(f : C [ c , c' ])(g : D [ d , d' ]) - → (×r d ⟪ f ⟫) ⋆⟨ _×C_ ⟩ (×l c' ⟪ g ⟫) - ≡ ×l c ⟪ g ⟫ ⋆⟨ _×C_ ⟩ ×r d' ⟪ f ⟫ - ×lr f g = ηEq Q Ax (combine-id×id f g) ∙ sym (ηEq Q Ax (combine-×id× f g)) - - -- C.id c ×ₑ D.id d - -- ≡ (C.id ⋆ C.id) ×ₑ (D.id ⋆ D.id) - -- ≡ (c × D .id) ⋆ (C .id × d) - -- ≡ id ⋆ id - simul-id : ∀ {c d} → - ηP Q Ax .I-hom (C .id {c} ×ₑ D .id {d}) ≡ _×C_ .id {c , d} - simul-id {c}{d} = - sym (ηEq Q Ax (combine-×id× (C .id) (D .id))) - ∙ cong₂ (comp' _×C_) (ηEq Q Ax (×id-Id c d)) ((ηEq Q Ax (id×-Id c d))) - ∙ _×C_ .⋆IdR (_×C_ .id) - - simul-comp : ∀ {c c' c'' d d' d''} - → (f : C [ c , c' ])(f' : C [ c' , c'' ]) - → (g : D [ d , d' ])(g' : D [ d' , d'' ]) - → ηP Q Ax .I-hom ((f ⋆⟨ C ⟩ f') ×ₑ (g ⋆⟨ D ⟩ g')) - ≡ (ηP Q Ax .I-hom (f ×ₑ g)) - ⋆⟨ _×C_ ⟩ (ηP Q Ax .I-hom (f' ×ₑ g')) - -- (f * f') × (g * g') - -- ≡ (f * f') × d ∘ c'' × (g ⋆ g') - -- ≡ ((f' × d) ∘ (f × d)) ∘ ((c'' × g') ∘ (c'' × g')) - -- ≡ ((f' × d) ∘ ((f × d) ∘ (c'' × g')) ∘ (c'' × g')) - -- ≡ ((f' × d) ∘ ((c' × g') ∘ (f × d')) ∘ (c'' × g')) - -- ≡ (f' × g') ∘ (f × g') - simul-comp f f' g g' = - sym (ηEq Q Ax (combine-id×id (f ⋆⟨ C ⟩ f') (g ⋆⟨ D ⟩ g') )) - ∙ cong₂ (seq' _×C_) (×r _ .F-seq f f') (×l _ .F-seq g g') - ∙ _×C_ .⋆Assoc (×r _ ⟪ f ⟫) (×r _ ⟪ f' ⟫) (×l _ ⟪ g ⟫ ⋆⟨ _×C_ ⟩ ×l _ ⟪ g' ⟫) - ∙ cong₂ (seq' _×C_) (refl {x = (×r _ ⟪ f ⟫)}) - (sym (_×C_ .⋆Assoc (×r _ ⟪ f' ⟫) (×l _ ⟪ g ⟫) (×l _ ⟪ g' ⟫)) - ∙ cong₂ (comp' _×C_) (refl {x = ×l _ ⟪ g' ⟫}) (×lr f' g) - ∙ (_×C_ .⋆Assoc (×l _ ⟪ g ⟫) (×r _ ⟪ f' ⟫) (×l _ ⟪ g' ⟫)) - ∙ cong₂ (seq' _×C_) - (refl {x = (×l _ ⟪ g ⟫)}) (ηEq Q Ax (combine-id×id f' g'))) - ∙ sym (_×C_ .⋆Assoc (×r _ ⟪ f ⟫) (×l _ ⟪ g ⟫) (ηP Q Ax .I-hom (f' ×ₑ g'))) - ∙ cong₂ (seq' _×C_) - (ηEq Q Ax (combine-id×id f g)) - (refl {x = (ηP Q Ax .I-hom (f' ×ₑ g'))}) - - -- todo: better name - ×× : Functor (C BP.×C D) _×C_ - ×× .F-ob (c , d) = (c , d) - ×× .F-hom (f , g) = ηP Q Ax .I-hom (f ×ₑ g) - ×× .F-id = simul-id - ×× .F-seq (f , g) (f' , g') = simul-comp f f' g g' - - -- UniversalBifunctor : Bifunctor C D _×C_ - -- UniversalBifunctor .Bif-ob = _,_ - -- UniversalBifunctor .Bif-homL f d = ×r d ⟪ f ⟫ - -- UniversalBifunctor .Bif-homR c g = ×l c ⟪ g ⟫ - -- UniversalBifunctor .Bif-idL = ×r _ .F-id - -- UniversalBifunctor .Bif-idR = ×l _ .F-id - -- UniversalBifunctor .Bif-seqL f f' = ×r _ .F-seq f f' - -- UniversalBifunctor .Bif-seqR g g' = ×l _ .F-seq g g' - -- UniversalBifunctor .Bif-assoc f g = ηEq Q Ax (commute f g) diff --git a/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc.agda b/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc.agda index 86a6e638..1411d2c9 100644 --- a/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc.agda +++ b/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc.agda @@ -17,7 +17,8 @@ import Cubical.Categories.Constructions.BinProduct.Redundant.Assoc.ToRight import Cubical.Categories.Constructions.BinProduct.Redundant.Assoc.ToLeft as ToLeft open import Cubical.Categories.Constructions.BinProduct.Redundant.Base as BP -open import Cubical.Categories.Constructions.Free.Category as Free hiding (rec) +open import Cubical.Categories.Constructions.Free.Category.Quiver as Free + hiding (rec) open import Cubical.Categories.Constructions.Presented as Presented hiding (rec) open import Cubical.Categories.Bifunctor.Redundant diff --git a/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToLeft.agda b/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToLeft.agda index 21c4f4b2..596ba4c1 100644 --- a/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToLeft.agda +++ b/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToLeft.agda @@ -13,7 +13,8 @@ open import Cubical.Data.Sum as Sum hiding (rec) open import Cubical.Data.Sigma open import Cubical.Categories.Constructions.BinProduct.Redundant.Base as BP -open import Cubical.Categories.Constructions.Free.Category as Free hiding (rec) +open import Cubical.Categories.Constructions.Free.Category.Quiver as Free + hiding (rec) open import Cubical.Categories.Constructions.Presented as Presented hiding (rec) open import Cubical.Categories.Bifunctor.Redundant as Bif diff --git a/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToRight.agda b/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToRight.agda index 3f377c7e..b1b650e4 100644 --- a/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToRight.agda +++ b/Cubical/Categories/Constructions/BinProduct/Redundant/Assoc/ToRight.agda @@ -13,7 +13,8 @@ open import Cubical.Data.Sum as Sum hiding (rec) open import Cubical.Data.Sigma open import Cubical.Categories.Constructions.BinProduct.Redundant.Base as BP -open import Cubical.Categories.Constructions.Free.Category as Free hiding (rec) +open import Cubical.Categories.Constructions.Free.Category.Quiver as Free + hiding (rec) open import Cubical.Categories.Constructions.Presented as Presented hiding (rec) open import Cubical.Categories.Bifunctor.Redundant diff --git a/Cubical/Categories/Constructions/BinProduct/Redundant/Base.agda b/Cubical/Categories/Constructions/BinProduct/Redundant/Base.agda index d39d24e4..fd1efb0c 100644 --- a/Cubical/Categories/Constructions/BinProduct/Redundant/Base.agda +++ b/Cubical/Categories/Constructions/BinProduct/Redundant/Base.agda @@ -15,7 +15,8 @@ open import Cubical.Data.Sum as Sum hiding (rec) open import Cubical.Data.Sigma import Cubical.Categories.Constructions.BinProduct as BP -open import Cubical.Categories.Constructions.Free.Category as Free hiding (rec) +open import Cubical.Categories.Constructions.Free.Category.Quiver as Free + hiding (rec) open import Cubical.Categories.Constructions.Presented as Presented hiding (rec) open import Cubical.Categories.Bifunctor.Redundant diff --git a/Cubical/Categories/Constructions/Elements/More.agda b/Cubical/Categories/Constructions/Elements/More.agda deleted file mode 100644 index c0612b58..00000000 --- a/Cubical/Categories/Constructions/Elements/More.agda +++ /dev/null @@ -1,37 +0,0 @@ -{-# OPTIONS --safe #-} - --- The Category of Elements - -open import Cubical.Categories.Category - -module Cubical.Categories.Constructions.Elements.More where - -open import Cubical.Categories.Instances.Sets -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Isomorphism -open import Cubical.Categories.Functor -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Data.Sigma -open import Cubical.Categories.Constructions.Elements - -import Cubical.Categories.Morphism as Morphism -import Cubical.Categories.Constructions.Slice as Slice - -open Category -open Functor - -module _ {ℓ ℓ'} {C : Category ℓ ℓ'} {ℓS} (F : Functor (C ^op) (SET ℓS)) where - open Contravariant {C = C} - Elementᴾ : Type (ℓ-max ℓ ℓS) - Elementᴾ = (∫ᴾ F) .ob - - ∫ᴾhomEqSimpl : ∀ {o1 o2} (f g : (∫ᴾ F) [ o1 , o2 ]) - → fst f ≡ fst g → f ≡ g - ∫ᴾhomEqSimpl f g p = ∫ᴾhomEq {F = F} f g refl refl p - - domain : Functor (∫ᴾ F) C - domain .F-ob (x , ϕ) = x - domain .F-hom (f , comm) = f - domain .F-id = refl - domain .F-seq f g = refl diff --git a/Cubical/Categories/Constructions/Free/Category.agda b/Cubical/Categories/Constructions/Free/Category/Quiver.agda similarity index 98% rename from Cubical/Categories/Constructions/Free/Category.agda rename to Cubical/Categories/Constructions/Free/Category/Quiver.agda index 94922ed6..0dcf44d3 100644 --- a/Cubical/Categories/Constructions/Free/Category.agda +++ b/Cubical/Categories/Constructions/Free/Category/Quiver.agda @@ -2,7 +2,7 @@ -- This time not using a graph as the presentation of the generators {-# OPTIONS --safe #-} -module Cubical.Categories.Constructions.Free.Category where +module Cubical.Categories.Constructions.Free.Category.Quiver where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Path diff --git a/Cubical/Categories/Constructions/Free/Functor.agda b/Cubical/Categories/Constructions/Free/Functor.agda deleted file mode 100644 index bd18f45a..00000000 --- a/Cubical/Categories/Constructions/Free/Functor.agda +++ /dev/null @@ -1,344 +0,0 @@ --- 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.Id hiding (_≡_; isSet; subst) - renaming (refl to reflId; _∙_ to _∙Id_; - transport to transportId; funExt to funExtId) -open import Cubical.Foundations.Path -open import Cubical.Foundations.Transport -open import Cubical.Foundations.GroupoidLaws -open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) -open import Cubical.Foundations.HLevels -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor.Base hiding (Id) -open import Cubical.Categories.NaturalTransformation.Base hiding (_⟦_⟧) -open import Cubical.Data.Graph.Base -open import Cubical.Data.Sigma - -open import Cubical.Data.Graph.Properties -open import Cubical.Data.Empty -open import Cubical.Categories.Constructions.Free.General as Free -open import Cubical.Categories.Constructions.Free.UnderlyingGraph - -open import Cubical.Tactics.CategorySolver.Reflection - -private - variable - ℓ ℓ' ℓc ℓc' ℓd ℓd' ℓg ℓg' ℓh ℓh' : Level - -open Category -open Functor -open NatTrans -open NatIso -open isIso - --- TODO: move these lemmas to Cubical.Foundations.Id -funExtRefl : ∀ {A : Type ℓ}{B : A → Type ℓ'} {f} → - Path (Id f f) (funExtId {A = A}{B = B}{f = f} - (λ x → reflId)) reflId -funExtRefl {A = A}{B = B}{f = f} = - congPath pathToId lem ∙ pathToIdRefl - where - lem : Path (Path ((x : A) → B x) f f) - (λ i x → idToPath {x = f x} reflId i) - (λ _ → f) - lem i j x = idToPathRefl {x = f x} i j - -substIdToPath : ∀ {A : Type ℓ}{B : A → Type ℓ'} {x y : A} (p : Id x y) - → subst B (idToPath p) ≡ transportId B p -substIdToPath {A = A}{B}{x = x} p = - funExt λ bx → J (λ by q → subst B (idToPath q) bx ≡ - transportId B q bx) (lem bx) p - where - lem : ∀ (bx : B x) → subst B (idToPath reflId) bx ≡ transportId B reflId bx - lem bx = (λ i → subst B (idToPathRefl i) bx) ∙ transportRefl bx - --- TODO: refactor this and the cat solver to use named modules -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 (Ugr FH) - Fϕ-homo $g x = ϕ x - Fϕ-homo <$g> x = F⟪ ↑ x ⟫ - - ηϕ : Id (Fϕ .F-ob ∘f ηG ._$g_) (ηH ._$g_ ∘f ϕ) - ηϕ = reflId - - module _ {𝓒 : Category ℓc ℓc'}{𝓓 : Category ℓd ℓd'} {𝓕 : Functor 𝓒 𝓓} where - module Semantics (ıG : Interp G 𝓒) (ıH : Interp H 𝓓) - (ıϕ : Id (𝓕 .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) = - transportId (λ (f : G .Node → 𝓓 .ob) → - 𝓓 [ f A , f B ]) ıϕ (𝓕 ⟪ semG ⟪ x ⟫ ⟫) - -- preserves 1-cells - 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 : transportId - (λ f → 𝓓 [ f A , f A ]) ıϕ (𝓕 ⟪ semG ⟪ idₑ ⟫ ⟫) ≡ 𝓓 .id - unbound = J (λ g p → - transportId (λ 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 : transportId - (λ f → 𝓓 [ f A , f C ]) ıϕ (𝓕 ⟪ semG ⟪ e ⋆ₑ e' ⟫ ⟫) - ≡ (transportId - (λ f → 𝓓 [ f A , f B ]) - ıϕ (𝓕 ⟪ semG ⟪ e ⟫ ⟫)) ⋆⟨ 𝓓 ⟩ - (transportId - (λ f → 𝓓 [ f B , f C ]) ıϕ (𝓕 ⟪ semG ⟪ e' ⟫ ⟫)) - unbound = J (λ g p → - transportId - (λ f → 𝓓 [ f A , f C ]) p (𝓕 ⟪ semG ⟪ e ⋆ₑ e' ⟫ ⟫) ≡ - (transportId (λ f → 𝓓 [ f A , f B ]) p (𝓕 ⟪ semG ⟪ e ⟫ ⟫)) - ⋆⟨ 𝓓 ⟩ (transportId (λ 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ϕ : Id (𝓕 ∘F semG) (semH ∘F Fϕ) - semϕ = - pathToId (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 - → Id {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 _ - (transportPath - (λ i → 𝓓 [ aoo-gen v 𝓕G Hϕ ıϕ i , - aoo-gen w 𝓕G Hϕ ıϕ i ]) (𝓕 ⟪ ıG <$g> e ⟫)) - (transportId (λ f → 𝓓 [ f v , f w ]) ıϕ (𝓕 ⟪ ıG <$g> e ⟫)) - lem = J (λ f p → Path _ - ((transportPath (λ i → - 𝓓 [ aoo-gen v 𝓕G f p i , - aoo-gen w 𝓕G f p i ]) (𝓕 ⟪ ıG <$g> e ⟫))) - ((transportId (λ 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𝓕 .F-ob : Id {G .Node → 𝓓 .ob} ((𝓕 ∘F arb𝓒) ∘Interp ηG) - (arb𝓒-agree : arb𝓒 ∘Interp ηG ≡ ıG) - (arb𝓓-agree : arb𝓓 ∘Interp ηH ≡ ıH) - (arb𝓕-agree : Square {A = G .Node → 𝓓 .ob} - (λ i x → arb𝓕 i ⟅ x ⟆) - (idToPath ıϕ) - (λ 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 = idToPath ıϕ - - aom-F : ∀ {v w} - → (e : FG [ v , w ]) - → PathP (λ i → 𝓓 [ (arb𝓓-agree i $g (ϕ v)) , - (arb𝓓-agree i $g (ϕ w)) ]) - (arb𝓓 ⟪ Fϕ ⟪ e ⟫ ⟫) - (transportId (λ (f : G .Node → 𝓓 .ob) → - 𝓓 [ f v , f w ]) ıϕ (𝓕 ⟪ semG ⟪ e ⟫ ⟫)) - aom-F {v}{w} e = - pathified ▷ λ i → substIdToPath {B = λ (f : G .Node → 𝓓 .ob) → - 𝓓 [ f v , f w ]} ıϕ i (𝓕 ⟪ semG ⟪ e ⟫ ⟫) - where - pathified : PathP - (λ i → 𝓓 [ arb𝓓-agree i $g ϕ v , arb𝓓-agree i $g ϕ w ]) - (arb𝓓 ⟪ Fϕ ⟪ e ⟫ ⟫) - (transportPath (λ 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 ⟆) - -- Square (λ i z → ıϕ i z) (λ i → _⟅_⟆ (semϕ' i)) - -- (λ i z → 𝓕 ⟅ sems-agree𝓒 (~ i) $g z ⟆) - -- (λ i x → sems-agree𝓓 (~ i) $g ϕ 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 - -- Just some isSet→SquareP nonsense - 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 - - -- sem-uniq-ϕ : Square arb𝓕 - -- (idToPath semϕ) - -- (λ i → 𝓕 ∘F sem-uniq-G i) - -- (λ i → sem-uniq-H i ∘F Fϕ) - -- sem-uniq-ϕ = {!!} diff --git a/Cubical/Categories/Constructions/Free/Functor/Uniqueness.agda b/Cubical/Categories/Constructions/Free/Functor/Uniqueness.agda deleted file mode 100644 index a4533344..00000000 --- a/Cubical/Categories/Constructions/Free/Functor/Uniqueness.agda +++ /dev/null @@ -1,210 +0,0 @@ --- Free functor between categories generated from two graphs --- -- and a homomorphism between them -{-# OPTIONS --safe --lossy-unification #-} -module Cubical.Categories.Constructions.Free.Functor.Uniqueness where - --- open import Cubical.Foundations.Prelude --- open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) --- open import Cubical.Foundations.HLevels --- open import Cubical.Categories.Category.Base --- open import Cubical.Categories.Functor.Base --- open import Cubical.Categories.NaturalTransformation.Base hiding (_⟦_⟧) --- open import Cubical.Data.Graph.Base - --- open import Cubical.Data.Graph.Properties --- open import Cubical.Data.Empty --- open import Cubical.Categories.Constructions.Free.General as --- Free hiding (module Semantics) --- open import Cubical.Categories.Constructions.Free.Functor.Base --- open import Cubical.Categories.Constructions.Free.UnderlyingGraph - --- open import Cubical.Tactics.CategorySolver.Reflection - --- open Category --- open Functor --- open NatTrans --- open NatIso --- open isIso - --- private --- variable --- ℓc ℓc' ℓd ℓd' ℓg ℓg' ℓh ℓh' : Level - --- module _ (G : Graph ℓg ℓg') (H : Graph ℓh ℓh') (ϕ : GraphHom G H) where --- -- show that the free functor generated from G , H and ϕ is initial --- -- this is a proof of the universal property of the free functor --- module _ {𝓒 : Category ℓc ℓc'}{𝓓 : Category ℓd ℓd'}(𝓕 : Functor 𝓒 𝓓) --- (ıG : GraphHom G (Ugr 𝓒)) (ıH : GraphHom H (Ugr 𝓓)) --- (ıϕ : InterpIso G 𝓓 (ıG ⋆Interp 𝓕) (ϕ ⋆GrHom ıH)) --- where --- open Semantics G H ϕ 𝓕 ıG ıH ıϕ - --- -- Let's say we had an alternative commuting square from Freeϕ to --- -- F that when composed with the universal interpretation agrees --- -- with some fixed interpretation ıϕ. Then in fact that square is --- -- isomorphic to the one generated from ıϕ --- module _ (sem𝓒' : Functor (FreeCat G) 𝓒) --- (sem𝓓' : Functor (FreeH+ϕ G H ϕ) 𝓓) --- (semϕ' : NatIso (𝓕 ∘F sem𝓒') (sem𝓓' ∘F (Freeϕ G H ϕ))) --- (sem𝓒'-agree : InterpIso G 𝓒 (sem𝓒' ∘Interp (η G)) ıG) --- (sem𝓓'-agree : InterpIso H 𝓓 (sem𝓓' ∘Interp (ηH G H ϕ)) ıH) --- (semϕ'-agree : (𝓕 ⊙ʳInterp symInterpIso sem𝓒'-agree ) --- ⋆InterpIso ((semϕ' ⊙ˡInterp (η G)) --- ⋆InterpIso ((sem𝓓' ⊙ʳInterp ηϕ G H ϕ) --- ⋆InterpIso (sem𝓓'-agree ∘ˡInterp ϕ))) --- ≡ ıϕ) --- where - --- -- first, sem𝓒 and sem𝓒' are isomorphic --- sem𝓒-iso : NatIso sem𝓒' sem𝓒 --- sem𝓒-iso = Free.Semantics.semIIso G 𝓒 ıG sem𝓒' sem𝓒'-agree - --- -- then, sem𝓓 and sem𝓓' are isomorphic --- private --- -- essentially, we have an iso that is natural on generators --- -- and we need to prove its natural on all terms --- α-mor = sem𝓓'-agree .fst .fst --- α-nat-generators = sem𝓓'-agree .fst .snd - --- α-nat-id : ∀ {v} → sem𝓓' ⟪ idf ⟫ ⋆⟨ 𝓓 ⟩ --- α-mor v ≡ α-mor v ⋆⟨ 𝓓 ⟩ 𝓓 .id --- α-nat-id = (λ i → sem𝓓' .F-id i ⋆⟨ 𝓓 ⟩ α-mor _) ∙ --- sym (idTrans (Id {C = 𝓓}) .N-hom _) - --- α-nat-seq : ∀ {u v w} → (e : FreeH+ϕ G H ϕ [ u , v ]) --- (e' : FreeH+ϕ G H ϕ [ v , w ]) --- → sem𝓓' ⟪ e ⟫ ⋆⟨ 𝓓 ⟩ α-mor _ ≡ α-mor _ ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ e ⟫ --- → sem𝓓' ⟪ e' ⟫ ⋆⟨ 𝓓 ⟩ α-mor _ ≡ α-mor _ ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ e' ⟫ --- → sem𝓓' ⟪ e ⋆f e' ⟫ ⋆⟨ 𝓓 ⟩ α-mor w ≡ α-mor _ ⋆⟨ 𝓓 ⟩ --- (sem𝓓 ⟪ e ⟫ ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ e' ⟫) --- α-nat-seq e e' e-ih e'-ih = --- (λ i → sem𝓓' .F-seq e e' i ⋆⟨ 𝓓 ⟩ α-mor _) --- ∙ 𝓓 .⋆Assoc _ _ _ --- ∙ cong (seq' 𝓓 (sem𝓓' ⟪ e ⟫)) e'-ih --- ∙ sym (𝓓 .⋆Assoc _ _ _) --- ∙ cong (comp' 𝓓 (sem𝓓 ⟪ e' ⟫)) e-ih --- ∙ 𝓓 .⋆Assoc _ _ _ - --- F⟪⟫-Functor : Functor (FreeCat G) (FreeH+ϕ G H ϕ) --- F⟪⟫-Functor .F-ob = ϕ ._$g_ --- F⟪⟫-Functor .F-hom = F⟪_⟫ --- F⟪⟫-Functor .F-id = F-idₑ --- F⟪⟫-Functor .F-seq = F-seqₑ - --- F⟪⟫-Freeϕ-agree : NatIso F⟪⟫-Functor (Freeϕ G H ϕ) --- F⟪⟫-Freeϕ-agree = --- Free.Semantics.semIIso G ((FreeH+ϕ G H ϕ)) --- (Freeϕ-homo G H ϕ) F⟪⟫-Functor (idInterpIso _ _) - --- natural-on-Freeϕ : NatIso (sem𝓓' ∘F Freeϕ G H ϕ) - -- (sem𝓓 ∘F Freeϕ G H ϕ) --- natural-on-Freeϕ = --- uniqueness-principle G (sem𝓓' ∘F Freeϕ G H ϕ) (sem𝓓 ∘F Freeϕ G H ϕ) --- ((sem𝓓' ⊙ʳInterp ηϕ G H ϕ) --- ⋆InterpIso ((sem𝓓'-agree ∘ˡInterp ϕ) ⋆InterpIso --- symInterpIso (sem𝓓 ⊙ʳInterp ηϕ G H ϕ))) - --- α-mor≡NatTransFreeϕ : ∀ {v} → --- (natural-on-Freeϕ ⊙ˡInterp (η G)) .fst .fst v ≡ α-mor (ϕ $g v) --- α-mor≡NatTransFreeϕ = --- (natural-on-Freeϕ ⊙ˡInterp (η G)) .fst .fst _ --- ≡[ i ]⟨ uniqueness-principle-restricts G - -- ((sem𝓓' ∘F Freeϕ G H ϕ)) --- ((sem𝓓 ∘F Freeϕ G H ϕ)) --- (((sem𝓓' ⊙ʳInterp ηϕ G H ϕ) ⋆InterpIso --- ((sem𝓓'-agree ∘ˡInterp ϕ) ⋆InterpIso symInterpIso --- (sem𝓓 ⊙ʳInterp ηϕ G H ϕ)))) i .fst .fst _ ⟩ --- (sem𝓓' ⟪ FreeH+ϕ G H ϕ .id ⟫ ⋆⟨ 𝓓 ⟩ --- (α-mor _ ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ FreeH+ϕ G H ϕ .id ⟫)) --- ≡[ i ]⟨ sem𝓓' .F-id i ⋆⟨ 𝓓 ⟩ (α-mor _ ⋆⟨ 𝓓 ⟩ sem𝓓 .F-id i) ⟩ --- (𝓓 .id ⋆⟨ 𝓓 ⟩ (α-mor _ ⋆⟨ 𝓓 ⟩ 𝓓 .id)) --- ≡⟨ solveCat! 𝓓 ⟩ --- α-mor _ ∎ - --- α-nat-F' : ∀ {u v} → (e : FreeCat G [ u , v ]) --- → sem𝓓' ⟪ Freeϕ G H ϕ ⟪ e ⟫ ⟫ ⋆⟨ 𝓓 ⟩ α-mor _ ≡ --- α-mor _ ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ Freeϕ G H ϕ ⟪ e ⟫ ⟫ --- α-nat-F' e = --- transport --- (λ i → sem𝓓' ⟪ Freeϕ G H ϕ ⟪ e ⟫ ⟫ ⋆⟨ 𝓓 ⟩ --- α-mor≡NatTransFreeϕ i ≡ α-mor≡NatTransFreeϕ i ⋆⟨ 𝓓 ⟩ --- sem𝓓 ⟪ Freeϕ G H ϕ ⟪ e ⟫ ⟫) - -- (natural-on-Freeϕ .trans .N-hom e) - --- -- Argument: α should be natural on everything --- -- of the form F ⟪ e ⟫ because ? --- α-nat-F : ∀ {u v} → (e : FreeCat G [ u , v ]) --- → sem𝓓' ⟪ F⟪ e ⟫ ⟫ ⋆⟨ 𝓓 ⟩ α-mor _ ≡ --- α-mor _ ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ F⟪ e ⟫ ⟫ --- α-nat-F e = --- sem𝓓' ⟪ F⟪ e ⟫ ⟫ ⋆⟨ 𝓓 ⟩ α-mor _ --- ≡[ i ]⟨ sem𝓓' ⟪ F⟪⟫-Freeϕ-agree⟪⟫ i ⟫ ⋆⟨ 𝓓 ⟩ α-mor _ ⟩ --- sem𝓓' ⟪ Freeϕ G H ϕ ⟪ e ⟫ ⟫ ⋆⟨ 𝓓 ⟩ α-mor _ --- ≡⟨ α-nat-F' e ⟩ --- α-mor _ ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ Freeϕ G H ϕ ⟪ e ⟫ ⟫ --- ≡[ i ]⟨ α-mor _ ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ F⟪⟫-Freeϕ-agree⟪⟫ (~ i) ⟫ ⟩ --- α-mor _ ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ F⟪ e ⟫ ⟫ ∎ --- where --- F⟪⟫-Freeϕ-agree⟪⟫ : F⟪ e ⟫ ≡ Freeϕ G H ϕ ⟪ e ⟫ --- F⟪⟫-Freeϕ-agree⟪⟫ = --- sym (FreeH+ϕ G H ϕ .⋆IdR F⟪ e ⟫) ∙ --- F⟪⟫-Freeϕ-agree .trans .N-hom _ ∙ FreeH+ϕ G H ϕ .⋆IdL _ - --- α-nat : ∀ {A B} (e : FreeH+ϕ G H ϕ [ A , B ]) --- → sem𝓓' ⟪ e ⟫ ⋆⟨ 𝓓 ⟩ α-mor B --- ≡ α-mor A ⋆⟨ 𝓓 ⟩ sem𝓓 ⟪ e ⟫ --- -- the actual cases --- α-nat (↑f x) = α-nat-generators x --- α-nat idf = α-nat-id --- α-nat (e ⋆f e') = α-nat-seq e e' (α-nat e) (α-nat e') --- α-nat F⟪ x ⟫ = α-nat-F x -- α-nat-F x --- -- 1-paths --- α-nat (⋆fIdL e i) j = --- isSet→SquareP (λ _ _ → 𝓓 .isSetHom) --- (α-nat-seq idf e α-nat-id (α-nat e)) --- (α-nat e) (λ i → seq' 𝓓 (sem𝓓' ⟪ ⋆fIdL e i ⟫) (α-mor _)) --- (λ i → seq' 𝓓 (α-mor _) (sem𝓓 ⟪ ⋆fIdL e i ⟫)) i j - --- α-nat (⋆fIdR e i) j = --- isSet→SquareP (λ _ _ → 𝓓 .isSetHom) --- (α-nat-seq e idf (α-nat e) α-nat-id) (α-nat e) --- (λ i → seq' 𝓓 (sem𝓓' ⟪ ⋆fIdR e i ⟫) (α-mor _)) --- (λ i → seq' 𝓓 (α-mor _) (sem𝓓 ⟪ ⋆fIdR e i ⟫)) i j - --- α-nat (⋆fAssoc e e' e'' i) j = --- isSet→SquareP (λ _ _ → 𝓓 .isSetHom) --- (α-nat-seq (e ⋆f e') e'' (α-nat-seq e e' (α-nat e) --- (α-nat e')) (α-nat e'')) --- (α-nat-seq e (e' ⋆f e'') (α-nat e) --- (α-nat-seq e' e'' (α-nat e') (α-nat e''))) --- (λ i → seq' 𝓓 (sem𝓓' ⟪ ⋆fAssoc e e' e'' i ⟫) (α-mor _)) --- (λ i → seq' 𝓓 (α-mor _) (sem𝓓 ⟪ ⋆fAssoc e e' e'' i ⟫)) i j --- α-nat (F-idₑ i) j = --- isSet→SquareP (λ _ _ → 𝓓 .isSetHom) (α-nat-F idₑ) (α-nat-id) --- (λ i → seq' 𝓓 (sem𝓓' ⟪ F-idₑ i ⟫) (α-mor (ϕ $g _))) --- (λ i → seq' 𝓓 (α-mor (ϕ $g _)) (sem𝓓 ⟪ F-idₑ i ⟫)) i j --- α-nat (F-seqₑ e e' i) j = --- isSet→SquareP (λ _ _ → 𝓓 .isSetHom) (α-nat-F (e ⋆ₑ e')) --- (α-nat-seq F⟪ e ⟫ F⟪ e' ⟫ (α-nat-F e) (α-nat-F e')) --- (λ i → seq' 𝓓 (sem𝓓' ⟪ F-seqₑ e e' i ⟫) (α-mor (ϕ $g _))) --- (λ i → seq' 𝓓 (α-mor (ϕ $g _)) (sem𝓓 ⟪ F-seqₑ e e' i ⟫)) i j - --- α-nat (F⟪⟫-ϕ-agree e i) j = --- isSet→SquareP (λ _ _ → 𝓓 .isSetHom) (α-nat-F (↑ e)) --- (α-nat-generators (ϕ <$g> e)) --- (λ i → seq' 𝓓 (sem𝓓' ⟪ F⟪⟫-ϕ-agree e i ⟫) (α-mor (ϕ $g _))) --- (λ i → seq' 𝓓 (α-mor (ϕ $g _)) (sem𝓓 ⟪ F⟪⟫-ϕ-agree e i ⟫)) i j --- -- the 2-path --- α-nat (isSetFExp e e' p q i j) = --- isSet→SquareP (λ i j → isSet→isGroupoid (𝓓 .isSetHom) --- (seq' 𝓓 (sem𝓓' ⟪ isSetFExp e e' p q i j ⟫) (α-mor _)) --- (seq' 𝓓 (α-mor _) (sem𝓓 ⟪ isSetFExp e e' p q i j ⟫))) --- (λ j → α-nat (p j)) (λ j → α-nat (q j)) (λ _ → α-nat e) --- (λ _ → α-nat e') i j - --- sem𝓓-trans : NatTrans sem𝓓' sem𝓓 --- sem𝓓-trans .N-ob = α-mor --- sem𝓓-trans .N-hom f = α-nat f --- sem𝓓-iso : NatIso sem𝓓' sem𝓓 --- sem𝓓-iso .trans = sem𝓓-trans --- sem𝓓-iso .nIso x = sem𝓓'-agree .snd x diff --git a/Cubical/Categories/Constructions/Free/General.agda b/Cubical/Categories/Constructions/Free/General.agda deleted file mode 100644 index 4d57f0a0..00000000 --- a/Cubical/Categories/Constructions/Free/General.agda +++ /dev/null @@ -1,157 +0,0 @@ --- Free category over a directed graph/quiver --- This time without any assumptions on the HLevels of the graph -{-# OPTIONS --safe #-} - -module Cubical.Categories.Constructions.Free.General where - -open import Cubical.Categories.Morphism -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Path -open import Cubical.Foundations.HLevels -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor.Base -open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧) -open import Cubical.Categories.NaturalTransformation.More -open import Cubical.Data.Graph.Base -open import Cubical.Data.Sigma - -open import Cubical.Data.Graph.Properties -open import Cubical.Categories.Constructions.Free.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 - 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 - - -- 2 categorical: induction is an equivalence - -- inductionIso : Iso (F ≡ F') (F ∘Interp η ≡ F' ∘Interp η) - -- inductionIso .fun p = λ i → p i ∘Interp η - -- inductionIso .inv = induction - -- inductionIso .rightInv = λ p → refl - -- inductionIso .leftInv p i = {!induction ?!} - -- inductionRefl : ∀ {𝓒 : Category ℓc ℓc'} (F : Functor FreeCat 𝓒) → - -- induction F F refl ≡ refl - -- inductionRefl = {!!} - module Semantics {ℓc ℓc'} (𝓒 : Category ℓc ℓc') - (ı : GraphHom G (Ugr 𝓒)) 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 𝓒} → ((Uhom F ∘GrHom η) ≡ ı) → F ≡ sem - sem-uniq {F} aog = induction F sem aog - - sem-contr : ∃![ F ∈ Functor FreeCat 𝓒 ] Uhom F ∘GrHom η ≡ ı - sem-contr .fst = sem , sem-extends-ı - sem-contr .snd (sem' , sem'-extends-ı) = ΣPathP paths - where - paths : Σ[ p ∈ sem ≡ sem' ] PathP (λ i → Uhom (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 (Ugr 𝓒) - ε : Functor FreeCat 𝓒 - ε = Semantics.sem 𝓒 (Uhom {𝓓 = 𝓒} Id) - - ε-reasoning : {𝓓 : Category ℓd ℓd'} - → (𝓕 : Functor 𝓒 𝓓) - → 𝓕 ∘F ε ≡ Semantics.sem 𝓓 (Uhom 𝓕) - ε-reasoning {𝓓 = 𝓓} 𝓕 = Semantics.sem-uniq 𝓓 (Uhom 𝓕) refl diff --git a/Cubical/Categories/Constructions/Free/UnderlyingGraph.agda b/Cubical/Categories/Constructions/Free/UnderlyingGraph.agda deleted file mode 100644 index 02f156fb..00000000 --- a/Cubical/Categories/Constructions/Free/UnderlyingGraph.agda +++ /dev/null @@ -1,262 +0,0 @@ -{-# OPTIONS --safe #-} - -module Cubical.Categories.Constructions.Free.UnderlyingGraph where - -open import Cubical.Categories.Morphism -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Categories.Category.Base -open import Cubical.Categories.Functor -open import Cubical.Categories.NaturalTransformation hiding (_⟦_⟧) -open import Cubical.Categories.NaturalTransformation.More -open import Cubical.Data.Graph.Base -open import Cubical.Data.Sigma -open import Cubical.Categories.Isomorphism - -open import Cubical.Data.Graph.Properties - -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 -Ugr : ∀ {ℓc ℓc'} (𝓒 : Category ℓc ℓc') → Graph ℓc ℓc' -Ugr 𝓒 .Node = 𝓒 .ob -Ugr 𝓒 .Edge = 𝓒 .Hom[_,_] - -Uhom : ∀ {ℓc ℓc' ℓd ℓd'} {𝓒 : Category ℓc ℓc'} - {𝓓 : Category ℓd ℓd'} (F : Functor 𝓒 𝓓) - → GraphHom (Ugr 𝓒) (Ugr 𝓓) -Uhom F ._$g_ = Functor.F-ob F -Uhom F ._<$g>_ = Functor.F-hom F - -module _ (G : Graph ℓg ℓg') (𝓒 : Category ℓc ℓc') where - Interp : Type _ - Interp = GraphHom G (Ugr 𝓒) - - InterpTrans : Interp → Interp → Type _ - InterpTrans ı ı' = - Σ[ f ∈ (∀ v → 𝓒 [ ı $g v , ı' $g v ])] - (∀ {v}{w}(e : G .Edge v w) → f w ∘⟨ 𝓒 ⟩ (ı <$g> e) ≡ ı' <$g> e ∘⟨ 𝓒 ⟩ f v) - - isInterpIso : {ı ı' : Interp} → InterpTrans ı ı' → Type (ℓ-max ℓg ℓc') - isInterpIso α = ∀ v → isIso 𝓒 (α .fst v) - - InterpIso : Interp → Interp → Type _ - InterpIso ı ı' = Σ (InterpTrans ı ı') isInterpIso - - idInterpIso : {ı : Interp} → InterpIso ı ı - idInterpIso .fst .fst v = 𝓒 .id - idInterpIso .fst .snd e = 𝓒 .⋆IdR _ ∙ sym (𝓒 .⋆IdL _) - idInterpIso .snd v = idCatIso .snd - - -- if 𝓒 is univalent, this should be an equivalence - pathToInterpIso : {ı ı' : Interp} → ı ≡ ı' → InterpIso ı ı' - pathToInterpIso {ı}{ı'} p = transport (λ i → InterpIso ı (p i)) idInterpIso - - isIsoInterpIso : {ı ı' : Interp} (α : InterpIso ı ı') → - ∀ v → CatIso 𝓒 (ı $g v) (ı' $g v) - isIsoInterpIso α v = (α .fst .fst v) , (α .snd v) - - _∘InterpIso_ : {ı ı' ı'' : Interp} → - InterpIso ı' ı'' → InterpIso ı ı' → InterpIso ı ı'' - (α ∘InterpIso β) .fst .fst v = α .fst .fst v ∘⟨ 𝓒 ⟩ β .fst .fst v - (α ∘InterpIso β) .fst .snd e = - sym (𝓒 .⋆Assoc _ _ _) - ∙ cong (comp' 𝓒 (α .fst .fst _)) (β .fst .snd e) - ∙ 𝓒 .⋆Assoc _ _ _ - ∙ cong (seq' 𝓒 (β .fst .fst _)) (α .fst .snd e) - ∙ sym (𝓒 .⋆Assoc _ _ _) - (α ∘InterpIso β) .snd v = - compIso (isIsoInterpIso α v) (isIsoInterpIso β v) .snd - - module InterpReasoning (ı : Interp) (ı' : Interp) (α : InterpIso ı ı') where - open isIso - sqRL : ∀ {v w} → {e : G .Edge v w} - → ı <$g> e ≡ α .fst .fst v ⋆⟨ 𝓒 ⟩ ı' <$g> e ⋆⟨ 𝓒 ⟩ α .snd w .inv - sqRL {v}{w}{e} = invMoveR (isIso→areInv (α .snd w)) (α .fst .snd e) - - -- copied from NaturalTransformation.Base - sqLL : ∀ {v w} → {e : G .Edge v w} - → ı' <$g> e ⋆⟨ 𝓒 ⟩ α .snd w .inv ≡ α .snd v .inv ⋆⟨ 𝓒 ⟩ (ı <$g> e) - sqLL {v}{w}{e} = - invMoveL (isIso→areInv (α .snd v)) (sym (sqRL ∙ 𝓒 .⋆Assoc _ _ _)) - -module _ {G : Graph ℓg ℓg'}{𝓒 : Category ℓc ℓc'} where - private - ITrans = InterpTrans G 𝓒 - IIso = InterpIso G 𝓒 - - InterpTrans≡ : ∀ {ı ı'}{α β : ITrans ı ı'} → - (∀ v → α .fst v ≡ β .fst v) → α ≡ β - InterpTrans≡ p = - Σ≡Prop (λ x → isPropImplicitΠ - (λ _ → isPropImplicitΠ - λ _ → isPropΠ (λ e → 𝓒 .isSetHom _ _))) (funExt p) - - - - InterpIso≡ : ∀ {ı ı'}{α β : IIso ı ı'} → - (∀ v → α .fst .fst v ≡ β .fst .fst v) → α ≡ β - InterpIso≡ p = Σ≡Prop (λ x → isPropΠ (λ x → isPropIsIso _)) (InterpTrans≡ p) - -seqInterpIso : ∀ {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'} - → {ı ı' ı'' : Interp G 𝓒} - → InterpIso G 𝓒 ı ı' - → InterpIso G 𝓒 ı' ı'' - → InterpIso G 𝓒 ı ı'' -seqInterpIso α α' = _∘InterpIso_ _ _ α' α - -_⋆InterpIso_ = seqInterpIso - -seqInterpIsoIdR : ∀ {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'} - → {ı ı' : Interp G 𝓒} - → (α : InterpIso G 𝓒 ı ı') - → (seqInterpIso α (idInterpIso _ _)) ≡ α -seqInterpIsoIdR {𝓒 = 𝓒} α = InterpIso≡ λ v → 𝓒 .⋆IdR _ - -seqInterpIsoIdL : ∀ {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'} - → {ı ı' : Interp G 𝓒} - → (α : InterpIso G 𝓒 ı ı') - → (seqInterpIso (idInterpIso _ _) α) ≡ α -seqInterpIsoIdL {𝓒 = 𝓒} α = InterpIso≡ λ v → 𝓒 .⋆IdL _ - -seqInterpIsoAssoc : ∀ {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'} - → {ı ı' ı'' ı''' : Interp G 𝓒} - → (α : InterpIso G 𝓒 ı ı') - → (α' : InterpIso G 𝓒 ı' ı'') - → (α'' : InterpIso G 𝓒 ı'' ı''') - → seqInterpIso (seqInterpIso α α') α'' ≡ - seqInterpIso α (seqInterpIso α' α'') -seqInterpIsoAssoc {𝓒 = 𝓒} α α' α'' = InterpIso≡ λ v → 𝓒 .⋆Assoc _ _ _ - -symInterpIso : ∀ {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'} - → {ı ı' : Interp G 𝓒} - → InterpIso G 𝓒 ı ı' - → InterpIso G 𝓒 ı' ı -symInterpIso α .fst .fst v = α .snd v .inv -symInterpIso α .fst .snd e = InterpReasoning.sqLL _ _ _ _ α -symInterpIso α .snd v .inv = α .fst .fst v -symInterpIso α .snd v .sec = α .snd v .ret -symInterpIso α .snd v .ret = α .snd v .sec - -symInterpIsoInvl : ∀ {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'} - → {ı ı' : Interp G 𝓒} - → (α : InterpIso G 𝓒 ı ı') - → seqInterpIso (symInterpIso α) α ≡ idInterpIso _ _ -symInterpIsoInvl α = InterpIso≡ (λ v → α .snd v .sec) - -symInterpIsoInvr : ∀ {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'} - → {ı ı' : Interp G 𝓒} - → (α : InterpIso G 𝓒 ı ı') - → seqInterpIso α (symInterpIso α) ≡ idInterpIso _ _ -symInterpIsoInvr α = InterpIso≡ (λ v → α .snd v .ret) - -symInterpIsoId : ∀ {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'} → {ı : Interp G 𝓒} - → symInterpIso {𝓒 = 𝓒} (idInterpIso _ _ {ı}) ≡ - idInterpIso _ _ {ı} -symInterpIsoId = InterpIso≡ (λ v → refl) - -_⋆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 - -module _ {G : Graph ℓg ℓg'}{H : Graph ℓh ℓh'} {𝓒 : Category ℓc ℓc'} where - -- homogeneous whiskering of an interpiso with a graph homomorphism - _∘ˡInterp_ : ∀ {ı ı' : Interp H 𝓒} (α : InterpIso H 𝓒 ı ı') - (ϕ : GraphHom G H) - → InterpIso G 𝓒 (ı ∘GrHom ϕ) (ı' ∘GrHom ϕ) - (α ∘ˡInterp ϕ) .fst .fst v = α .fst .fst (ϕ $g v) - (α ∘ˡInterp ϕ) .fst .snd e = α .fst .snd (ϕ <$g> e) - (α ∘ˡInterp ϕ) .snd v = α .snd (ϕ $g v) - -module _ {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'}{𝓓 : Category ℓd ℓd'} where - -- "heterogeneous" whiskering of an interprIso with a functor - _⊙ʳInterp_ : ∀ (K : Functor 𝓒 𝓓) {ı ı' : Interp G 𝓒} → - (α : InterpIso G 𝓒 ı ı') - → InterpIso G 𝓓 (K ∘Interp ı) (K ∘Interp ı') - (K ⊙ʳInterp α) .fst .fst v = K ⟪ α .fst .fst v ⟫ - (K ⊙ʳInterp α) .fst .snd e = preserveCommF {F = K}(α .fst .snd e) - (K ⊙ʳInterp α) .snd v = preserveIsosF {F = K} (isIsoInterpIso _ _ α v) .snd - - ⊙ʳInterp-IdIso : ∀ {K : Functor 𝓒 𝓓}{ı : Interp G 𝓒} → - K ⊙ʳInterp (idInterpIso _ _ {ı}) ≡ idInterpIso _ _ - ⊙ʳInterp-IdIso {K} = InterpIso≡ λ v → K .F-id - - ⊙ʳInterp-CompIso : ∀ {K : Functor 𝓒 𝓓}{ı ı' ı'' : Interp G 𝓒} - (α : InterpIso _ _ ı ı') (β : InterpIso _ _ ı' ı'') - → K ⊙ʳInterp (α ⋆InterpIso β) ≡ - (K ⊙ʳInterp α) ⋆InterpIso (K ⊙ʳInterp β) - ⊙ʳInterp-CompIso {K} α β = InterpIso≡ λ v → K .F-seq _ _ - - -- "heterogeneous" whiskering of an interpretation with a natural isomorphism - _⊙ˡInterp_ : ∀ {F F' : Functor 𝓒 𝓓} (α : NatIso F F') - (ı : Interp G 𝓒) → InterpIso G 𝓓 (F ∘Interp ı) (F' ∘Interp ı) - (α ⊙ˡInterp ı) .fst .fst v = α .trans .N-ob (ı $g v) - (α ⊙ˡInterp ı) .fst .snd e = α .trans .N-hom (ı <$g> e) - (α ⊙ˡInterp ı) .snd v = α .nIso (ı $g v) - - ⊙ˡInterp-Seq : ∀ {F F' F'' : Functor 𝓒 𝓓} - (α : NatIso F F')(α' : NatIso F' F'') (ı : Interp G 𝓒) - → (seqNatIso α α') ⊙ˡInterp ı ≡ seqInterpIso (α ⊙ˡInterp ı) (α' ⊙ˡInterp ı) - ⊙ˡInterp-Seq α α' ı = InterpIso≡ λ v → refl - - ⊙ˡInterp-Sym : ∀ {F F' : Functor 𝓒 𝓓} (α : NatIso F F') (ı : Interp G 𝓒) - → symNatIso α ⊙ˡInterp ı ≡ symInterpIso (α ⊙ˡInterp ı) - ⊙ˡInterp-Sym α ı = InterpIso≡ (λ v → refl) - - ⊙ˡInterp-Id : ∀ {F : Functor 𝓒 𝓓} (ı : Interp G 𝓒) - → idNatIso F ⊙ˡInterp ı ≡ idInterpIso _ _ - ⊙ˡInterp-Id ı = InterpIso≡ (λ v → refl) - - private - _∙I_ : ∀ {ı ı' ı'' : Interp G 𝓓} → InterpIso G 𝓓 ı ı' → - InterpIso G 𝓓 ı' ı'' → InterpIso G 𝓓 ı ı'' - α ∙I β = _∘InterpIso_ G 𝓓 β α - - -- "parallel" composition of a natural isomorphism and an interp isomorphism - _⊙Interp_ : ∀ {F F' : Functor 𝓒 𝓓} (α : NatIso F F') - {ı ı' : Interp G 𝓒} → (β : InterpIso _ 𝓒 ı ı') → - InterpIso G 𝓓 (F ∘Interp ı) (F' ∘Interp ı') - _⊙Interp_ {F}{F'} α {ı}{ı'} β = (F ⊙ʳInterp β) ∙I (α ⊙ˡInterp ı') - - -⊙ʳInterpIdF : {G : Graph ℓg ℓg'}{𝓒 : Category ℓc ℓc'} {ı ı' : Interp G 𝓒} → - (α : InterpIso G 𝓒 ı ı') - → Id ⊙ʳInterp α ≡ α -⊙ʳInterpIdF α = InterpIso≡ (λ v → refl) - -⊙ʳInterpCompF : {G : Graph ℓg ℓg'}{𝓒 : Category ℓc ℓc'} - {𝓓 : Category ℓd ℓd'}{𝓔 : Category ℓe ℓe'} - (K : Functor 𝓓 𝓔) (J : Functor 𝓒 𝓓) - {ı ı' : Interp G 𝓒} → (α : InterpIso G 𝓒 ı ı') - → (K ∘F J) ⊙ʳInterp α ≡ K ⊙ʳInterp (J ⊙ʳInterp α) -⊙ʳInterpCompF K J α = InterpIso≡ λ v → refl - -∘ʳ⊙ˡ≡⊙ʳ⊙ˡ : {G : Graph ℓg ℓg'} {𝓒 : Category ℓc ℓc'} - (ı : Interp G 𝓒) - {𝓓 : Category ℓd ℓd'} {F F' : Functor 𝓒 𝓓} - (α : NatIso F F') - {𝓔 : Category ℓe ℓe'} - (K : Functor 𝓓 𝓔) - → (K ∘ʳi α) ⊙ˡInterp ı ≡ K ⊙ʳInterp (α ⊙ˡInterp ı) -∘ʳ⊙ˡ≡⊙ʳ⊙ˡ ı α K = refl diff --git a/Cubical/Categories/Constructions/Lift.agda b/Cubical/Categories/Constructions/Lift.agda deleted file mode 100644 index 8527ad07..00000000 --- a/Cubical/Categories/Constructions/Lift.agda +++ /dev/null @@ -1,37 +0,0 @@ -{-# 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 deleted file mode 100644 index 7ae05234..00000000 --- a/Cubical/Categories/Constructions/Power.agda +++ /dev/null @@ -1,29 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Categories.Constructions.Power where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Structure -open import Cubical.Categories.Category -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Functor -open import Cubical.Categories.Constructions.Product -open import Cubical.Categories.Constructions.Product.More - -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/Presented.agda b/Cubical/Categories/Constructions/Presented.agda index 4ff8d529..e39c59fa 100644 --- a/Cubical/Categories/Constructions/Presented.agda +++ b/Cubical/Categories/Constructions/Presented.agda @@ -15,7 +15,7 @@ open import Cubical.HITs.PropositionalTruncation hiding (rec) open import Cubical.HITs.SetQuotients as Quotient renaming ([_] to [_]q) hiding (rec) -open import Cubical.Categories.Constructions.Free.Category as Free +open import Cubical.Categories.Constructions.Free.Category.Quiver as Free hiding (rec; ind) private variable diff --git a/Cubical/Categories/Constructions/Product/More.agda b/Cubical/Categories/Constructions/Product/More.agda deleted file mode 100644 index f8b5447e..00000000 --- a/Cubical/Categories/Constructions/Product/More.agda +++ /dev/null @@ -1,30 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Categories.Constructions.Product.More where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Structure -open import Cubical.Categories.Category -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Functor -open import Cubical.Categories.Constructions.Product - -private - variable - ℓA ℓC ℓC' ℓD ℓD' : Level -open Functor -module _ (A : Type ℓA) (catC : A → Category ℓC ℓC') where - Π-intro : {D : Category ℓD ℓD'} → - (∀ (a : A) → Functor D (catC a)) → Functor D (ΠC A catC) - Π-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 : A) → Functor (ΠC A catC) (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 - --- TODO: if each of the catCs is univalent then so is the product diff --git a/Cubical/Categories/Exponentials.agda b/Cubical/Categories/Exponentials.agda index 6b1d3fcf..6da248da 100644 --- a/Cubical/Categories/Exponentials.agda +++ b/Cubical/Categories/Exponentials.agda @@ -3,6 +3,7 @@ module Cubical.Categories.Exponentials where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv open import Cubical.Categories.Category open import Cubical.Categories.Constructions.BinProduct.Redundant.Base open import Cubical.Categories.Bifunctor.Redundant @@ -21,8 +22,8 @@ private ℓC ℓC' : Level open Category -open UnivElt -open isUniversal +open UniversalElement +open isEquiv module _ (C : Category ℓC ℓC') where Exponential : (c d : C .ob) → (∀ (e : C .ob) → BinProduct C c e) → Type _ @@ -34,14 +35,14 @@ module _ (C : Category ℓC ℓC') where Exponentials = 2VarRightAdjointL C C C ×Bif ExponentialF : Exponentials → Functor ((C ^op) ×C C) C - ExponentialF exps = ParamUnivElt→ProfRepresentation _ _ _ exps .fst + ExponentialF exps = FunctorComprehension _ _ _ exps .fst module ExpNotation (exp : Exponentials) where _⇒_ : C .ob → C .ob → C .ob c ⇒ d = exp (c , d) .vertex lda : ∀ {Γ c d} → C [ Γ × c , d ] → C [ Γ , c ⇒ d ] - lda f = exp _ .universal .coinduction f + lda f = exp _ .universal _ .equiv-proof f .fst .fst app : ∀ {c d} → C [ (c ⇒ d) × c , d ] app = exp _ .element diff --git a/Cubical/Categories/Instances/Functors/More.agda b/Cubical/Categories/Instances/Functors/More.agda index 6c6e13e7..50e40475 100644 --- a/Cubical/Categories/Instances/Functors/More.agda +++ b/Cubical/Categories/Instances/Functors/More.agda @@ -30,24 +30,6 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where open Functor open NatTrans - appF : Functor ((FUNCTOR C D) ×C C) D - appF .F-ob (F , c) = F ⟅ c ⟆ - appF .F-hom {x = (F , c)}{y = (F' , c')} (α , f) = F ⟪ f ⟫ ⋆⟨ D ⟩ α .N-ob c' - appF .F-id {x = (F , c)} = - ((F ⟪ C .id ⟫ ⋆⟨ D ⟩ D .id)) ≡⟨ (λ i → F .F-id i ⋆⟨ D ⟩ D .id) ⟩ - (D .id ⋆⟨ D ⟩ D .id) ≡⟨ D .⋆IdR (D .id) ⟩ - (D .id) ∎ - appF .F-seq {x = (F , c)}{y = (F' , c')}{z = (F'' , c'')}(α , f) (α' , f') = - F ⟪ f ⋆⟨ C ⟩ f' ⟫ ⋆⟨ D ⟩ (α .N-ob _ ⋆⟨ D ⟩ α' .N-ob c'') - ≡⟨ (λ i → F .F-seq f f' i ⋆⟨ D ⟩ (α .N-ob _ ⋆⟨ D ⟩ α' .N-ob c'')) ⟩ - F ⟪ f ⟫ ⋆⟨ D ⟩ F ⟪ f' ⟫ ⋆⟨ D ⟩ (α .N-ob _ ⋆⟨ D ⟩ α' .N-ob c'') - ≡⟨ solveCat! D ⟩ - F ⟪ f ⟫ ⋆⟨ D ⟩ ((F ⟪ f' ⟫ ⋆⟨ D ⟩ α .N-ob _) ⋆⟨ D ⟩ α' .N-ob c'') - ≡⟨ (λ i → F ⟪ f ⟫ ⋆⟨ D ⟩ (α .N-hom f' i ⋆⟨ D ⟩ α' .N-ob c'')) ⟩ - F ⟪ f ⟫ ⋆⟨ D ⟩ ((α .N-ob _ ⋆⟨ D ⟩ F' ⟪ f' ⟫) ⋆⟨ D ⟩ α' .N-ob c'') - ≡⟨ solveCat! D ⟩ - (F ⟪ f ⟫ ⋆⟨ D ⟩ α .N-ob c') ⋆⟨ D ⟩ (F' ⟪ f' ⟫ ⋆⟨ D ⟩ α' .N-ob c'') ∎ - module _ {Γ : Category ℓΓ ℓΓ'} where -- The action of currying out the right argument of a Functor (Γ ×C C) D λFr : Functor (Γ ×C C) D → Functor Γ (FUNCTOR C D) diff --git a/Cubical/Categories/Instances/Sets/More.agda b/Cubical/Categories/Instances/Sets/More.agda index 7e1994c9..edc51f43 100644 --- a/Cubical/Categories/Instances/Sets/More.agda +++ b/Cubical/Categories/Instances/Sets/More.agda @@ -9,6 +9,7 @@ open import Cubical.Data.Sigma open import Cubical.Categories.Category open import Cubical.Categories.Functor +open import Cubical.Categories.Bifunctor.Redundant open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Constructions.BinProduct @@ -17,15 +18,18 @@ private ℓ ℓ' : Level open Functor --- 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 +×SetsBif : Bifunctor (SET ℓ) (SET ℓ) (SET ℓ) +×SetsBif = mkBifunctorParAx F where + open BifunctorParAx + F : BifunctorParAx (SET ℓ) (SET ℓ) (SET ℓ) + F .Bif-ob A B = ⟨ A ⟩ × ⟨ B ⟩ , isSet× (A .snd) (B .snd) + F .Bif-homL f B (x , y) = f x , y + F .Bif-homR A g (x , y) = x , (g y) + F .Bif-hom× f g (x , y) = (f x) , (g y) + F .Bif-×-id = refl + F .Bif-×-seq f f' g g' = refl + F .Bif-L×-agree f = refl + F .Bif-R×-agree g = refl -×Sets : Functor (SET ℓ ×C SET ℓ) (SET ℓ) -×Sets .F-ob (A , B) = ⟨ A ⟩ × ⟨ B ⟩ , isSet× (A .snd) (B .snd) -×Sets .F-hom (f , g) (x , y) = (f x) , (g y) -×Sets .F-id = refl -×Sets .F-seq f g = refl +×Sets : Functor ((SET ℓ) ×C (SET ℓ)) (SET ℓ) +×Sets = BifunctorToParFunctor ×SetsBif diff --git a/Cubical/Categories/Limits/BinProduct/More.agda b/Cubical/Categories/Limits/BinProduct/More.agda index 14d3e19d..385af441 100644 --- a/Cubical/Categories/Limits/BinProduct/More.agda +++ b/Cubical/Categories/Limits/BinProduct/More.agda @@ -2,6 +2,7 @@ module Cubical.Categories.Limits.BinProduct.More 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 hiding (_×_) @@ -15,37 +16,39 @@ open import Cubical.Categories.Functors.Constant open import Cubical.Categories.Functor open import Cubical.Categories.Profunctor.General open import Cubical.Categories.Isomorphism +open import Cubical.Categories.Instances.Sets.More open import Cubical.Categories.Limits.BinProduct open import Cubical.Categories.Presheaf.Representable open import Cubical.Categories.Adjoint.UniversalElements -open import Cubical.Categories.Bifunctor.Base -import Cubical.Categories.Bifunctor.Redundant as R +open import Cubical.Categories.Bifunctor.Redundant as R + +open import Cubical.Categories.Presheaf.More private variable ℓ ℓ' : Level open Iso -open UnivElt -open isUniversal +open UniversalElement open BinProduct open Category open Functor +open Bifunctor +open isEquiv module _ (C : Category ℓ ℓ') where BinProductToRepresentable : ∀ {a b} → BinProduct C a b → RightAdjointAt _ _ (Δ C) (a , b) BinProductToRepresentable bp .vertex = bp .binProdOb BinProductToRepresentable bp .element = (bp .binProdPr₁) , (bp .binProdPr₂) - BinProductToRepresentable bp .universal .coinduction (f1 , f2) = + BinProductToRepresentable bp .universal A .equiv-proof (f1 , f2) .fst .fst = bp .univProp f1 f2 .fst .fst - BinProductToRepresentable bp .universal .commutes (f1 , f2) = - cong₂ _,_ (up .fst .snd .fst) (up .fst .snd .snd) - where up = bp .univProp f1 f2 - BinProductToRepresentable bp .universal .is-uniq (f1 , f2) fp commutes = - cong fst - (sym (bp .univProp f1 f2 .snd - (fp , cong fst commutes , cong snd commutes))) + BinProductToRepresentable bp .universal A .equiv-proof (f1 , f2) .fst .snd = + cong₂ _,_ (bp .univProp f1 f2 .fst .snd .fst) + ((bp .univProp f1 f2 .fst .snd .snd)) + BinProductToRepresentable bp .universal A .equiv-proof (f1 , f2) .snd y = + Σ≡Prop (λ _ → isSet× (isSetHom C) (isSetHom C) _ _) + (cong fst (bp .univProp f1 f2 .snd ((y .fst) , PathPΣ (y .snd)))) module _ (bp : BinProducts C) where BinProductsToUnivElts : RightAdjoint C (C ×C C) (Δ C) @@ -54,8 +57,11 @@ module _ (C : Category ℓ ℓ') where ProdProf : C o-[ ℓ' ]-* (C ×C C) ProdProf = Functor→Profo-* C (C ×C C) (Δ C) + ProdProf' : C o-[ (ℓ-max ℓ ℓ') ]-* (C R.×C C) + ProdProf' = Functor→Profo-* C (C R.×C C) (R.ProdToRedundant C C ∘F Δ C) + BinProductF : Functor (C ×C C) C - BinProductF = ParamUnivElt→Functor _ _ _ BinProductsToUnivElts + BinProductF = FunctorComprehension _ _ _ BinProductsToUnivElts .fst private variable @@ -63,24 +69,27 @@ module _ (C : Category ℓ ℓ') where f g h : C [ a , b ] module _ {a} (bp : ∀ b → BinProduct C a b) where - -- ProdAProf [ c , b ] = C^2 [ (c , c) , (a , b) ] + -- ProdAProf [ c , b ] = C [ c , a ] × C [ c , b ] ProdAProf : C o-[ ℓ' ]-* C - ProdAProf = _o×_ {C = C} (pAppR (HomBif C) a) (HomBif C) + ProdAProf = _o×_ {C = C} (appR (HomBif C) a) (HomBif C) - BinProductWithToRepresentable : ParamUnivElt C C ProdAProf + BinProductWithToRepresentable : UniversalElements C C ProdAProf BinProductWithToRepresentable b .vertex = bp b .binProdOb BinProductWithToRepresentable b .element .fst = bp b .binProdPr₁ BinProductWithToRepresentable b .element .snd = bp b .binProdPr₂ - BinProductWithToRepresentable b .universal .coinduction (f1 , f2) = - bp b .univProp f1 f2 .fst .fst - BinProductWithToRepresentable b .universal .commutes (f1 , f2) = - cong₂ _,_ (up .fst .snd .fst) (up .fst .snd .snd) - where up = bp b .univProp f1 f2 - BinProductWithToRepresentable b .universal .is-uniq (f1 , f2) fp commutes = - cong fst (sym (bp b .univProp f1 f2 .snd - (fp , cong fst commutes , cong snd commutes))) - - BinProductWithF = ParamUnivElt→Functor _ _ _ BinProductWithToRepresentable + BinProductWithToRepresentable b .universal c .equiv-proof (f1 , f2) + .fst .fst = bp b .univProp f1 f2 .fst .fst + BinProductWithToRepresentable b .universal c .equiv-proof (f1 , f2) + .fst .snd = + cong₂ _,_ (bp b .univProp f1 f2 .fst .snd .fst) + (bp b .univProp f1 f2 .fst .snd .snd) + BinProductWithToRepresentable b .universal c .equiv-proof (f1 , f2) .snd y = + Σ≡Prop + (λ x → isSet× (isSetHom C) (isSetHom C) _ _) + (cong fst ( bp b .univProp f1 f2 .snd ((y .fst) , PathPΣ (y .snd)))) + + BinProductWithF = + FunctorComprehension _ _ _ BinProductWithToRepresentable .fst _ : ∀ {b b'}(f : C [ b , b' ]) → BinProductWithF ⟪ f ⟫ ≡ @@ -88,6 +97,7 @@ module _ (C : Category ℓ ℓ') where (f ∘⟨ C ⟩ bp b .binProdPr₂) .fst .fst _ = λ f → refl module ProdsWithNotation where + open UniversalElementNotation {C = C} private ues = BinProductWithToRepresentable a×_ : C .ob → C .ob @@ -103,36 +113,36 @@ module _ (C : Category ℓ ℓ') where -- which should follow by general fact that universal elements are natural _,p_ : C [ c , a ] → C [ c , b ] → C [ c , a× b ] - f ,p g = ues _ .universal .coinduction (f , g) + f ,p g = ues _ .universal _ .equiv-proof (f , g) .fst .fst ×pF = BinProductWithF ×p_ : C [ b , c ] → C [ a× b , a× c ] ×p_ = BinProductWithF .F-hom ×β₁ : π₁ ∘⟨ C ⟩ (f ,p g) ≡ f - ×β₁ = cong fst (ues _ .universal .commutes _) + ×β₁ = cong fst (ues _ .universal _ .equiv-proof _ .fst .snd) ×β₂ : π₂ ∘⟨ C ⟩ (f ,p g) ≡ g - ×β₂ = cong snd (ues _ .universal .commutes _) + ×β₂ = cong snd (ues _ .universal _ .equiv-proof _ .fst .snd) ×η : f ≡ ((π₁ ∘⟨ C ⟩ f) ,p (π₂ ∘⟨ C ⟩ f)) - ×η = η-expansion (ues _ .universal) _ + ×η = η (ues _) ×η' : C .id {x = a× b} ≡ (π₁ ,p π₂) - ×η' = coinduction-elt (ues _ .universal) + ×η' = weak-η (ues _) ,p-natural : ( f ,p g ) ∘⟨ C ⟩ h ≡ ((f ∘⟨ C ⟩ h) ,p (g ∘⟨ C ⟩ h)) - ,p-natural = coinduction-natural (ues _ .universal) _ _ + ,p-natural = intro-natural (ues _) ×-extensionality : π₁ ∘⟨ C ⟩ f ≡ π₁ ∘⟨ C ⟩ g → π₂ ∘⟨ C ⟩ f ≡ π₂ ∘⟨ C ⟩ g → f ≡ g - ×-extensionality p1 p2 = - determined-by-elt (ues _ .universal) (cong₂ _,_ p1 p2) + ×-extensionality p1 p2 = extensionality (ues _) (ΣPathP (p1 , p2)) module Notation (bp : BinProducts C) where private ues : RightAdjointAt C (C ×C C) (Δ C) (a , b) ues = BinProductsToUnivElts bp _ + open UniversalElementNotation {C = C} _×_ : C .ob → C .ob → C .ob a × b = bp a b .binProdOb @@ -177,26 +187,24 @@ module _ (C : Category ℓ ℓ') where _ = refl ×β₁ : π₁ ∘⟨ C ⟩ (f ,p g) ≡ f - ×β₁ {f = f}{g = g} = bp _ _ .univProp f g .fst .snd .fst + ×β₁ {f = f}{g = g} = cong fst (β ues) ×β₂ : π₂ ∘⟨ C ⟩ (f ,p g) ≡ g - ×β₂ {f = f}{g = g} = bp _ _ .univProp f g .fst .snd .snd + ×β₂ {f = f}{g = g} = cong snd (β ues) ×η : f ≡ ((π₁ ∘⟨ C ⟩ f) ,p (π₂ ∘⟨ C ⟩ f)) - ×η {f = f} = η-expansion (ues .universal) f + ×η {f = f} = η ues ×η' : C .id {a × b} ≡ (π₁ ,p π₂) - ×η' = coinduction-elt (ues .universal) + ×η' = weak-η ues ,p-natural : ( f ,p g ) ∘⟨ C ⟩ h ≡ ((f ∘⟨ C ⟩ h) ,p (g ∘⟨ C ⟩ h)) - ,p-natural {f = f}{g = g}{h = h} = - coinduction-natural (ues .universal) (f , g) h + ,p-natural {f = f}{g = g}{h = h} = intro-natural ues -- this has the benefit of always applying ×-extensionality : π₁ ∘⟨ C ⟩ f ≡ π₁ ∘⟨ C ⟩ g → π₂ ∘⟨ C ⟩ f ≡ π₂ ∘⟨ C ⟩ g → f ≡ g - ×-extensionality p1 p2 = - determined-by-elt (ues .universal) (cong₂ _,_ p1 p2) + ×-extensionality p1 p2 = extensionality ues (ΣPathP (p1 , p2)) module _ (Γ : C .ob) where module PWN = ProdsWithNotation (bp Γ) diff --git a/Cubical/Categories/Limits/Terminal/More.agda b/Cubical/Categories/Limits/Terminal/More.agda index a66486f4..f74d49c0 100644 --- a/Cubical/Categories/Limits/Terminal/More.agda +++ b/Cubical/Categories/Limits/Terminal/More.agda @@ -15,13 +15,6 @@ private variable ℓ ℓ' ℓc ℓc' ℓd ℓd' : Level -isoToTerminal : ∀ (C : Category ℓ ℓ') (x : Terminal C) y → - CatIso C (terminalOb C x) y → isTerminal C y -isoToTerminal C x y x≅y y' .fst = x≅y .fst ∘⟨ C ⟩ terminalArrow C x y' -isoToTerminal C x y x≅y y' .snd f = - sym (⋆InvRMove (invIso x≅y) - (sym (terminalArrowUnique C {T = x} (invIso x≅y .fst ∘⟨ C ⟩ f)))) - preservesTerminal : ∀ (C : Category ℓc ℓc')(D : Category ℓd ℓd') → Functor C D → Type (ℓ-max (ℓ-max (ℓ-max ℓc ℓc') ℓd) ℓd') diff --git a/Cubical/Categories/Monad/Algebra.agda b/Cubical/Categories/Monad/Algebra.agda index cfa491a0..e8b0470d 100644 --- a/Cubical/Categories/Monad/Algebra.agda +++ b/Cubical/Categories/Monad/Algebra.agda @@ -3,6 +3,8 @@ module Cubical.Categories.Monad.Algebra where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.HLevels open import Cubical.Data.Sigma open import Cubical.Categories.Category @@ -14,6 +16,8 @@ open import Cubical.Categories.Constructions.BinProduct open import Cubical.Categories.Monad.ExtensionSystem open import Cubical.Categories.Adjoint.UniversalElements +open import Cubical.Foundations.Isomorphism.More + private variable ℓ ℓ' : Level @@ -98,17 +102,15 @@ module _ {C : Category ℓ ℓ'} (M : ExtensionSystem C) where Underlying .F-seq f g = refl open import Cubical.Categories.Presheaf.Representable - open UnivElt - open isUniversal + open UniversalElement + open isEquiv Free : LeftAdjoint ALGEBRA C Underlying Free c .vertex = FreeAlgebra c Free c .element = η - Free c .universal .coinduction {β} f = - (β .snd .bindA f) , λ g → β .snd .bindA-comp - Free c .universal .commutes {β} f = β .snd .bindA-l - Free c .universal .is-uniq {β} ϕ (ψ , ψ-homo) x = - AlgebraHom≡ {FreeAlgebra _}{β} ((ψ , ψ-homo)) - ((β .snd .bindA ϕ) , λ g → β .snd .bindA-comp) - ( (sym (C .⋆IdL _) ∙ cong₂ (seq' C) (sym bind-r) refl) - ∙ ψ-homo η - ∙ cong (β .snd .bindA) x) + Free c .universal β = isIsoToIsEquiv + ( (λ f → β .snd .bindA f , λ _ → β .snd .bindA-comp) + , (λ f → β .snd .bindA-l) + , λ ϕ → AlgebraHom≡ {FreeAlgebra _}{β} _ _ + ( sym (ϕ .snd η) + ∙ cong (comp' C _) bind-r + ∙ C .⋆IdL _)) diff --git a/Cubical/Categories/Monad/ExtensionSystem.agda b/Cubical/Categories/Monad/ExtensionSystem.agda index 289af49c..b16c27f5 100644 --- a/Cubical/Categories/Monad/ExtensionSystem.agda +++ b/Cubical/Categories/Monad/ExtensionSystem.agda @@ -7,6 +7,7 @@ module Cubical.Categories.Monad.ExtensionSystem where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.HLevels open import Cubical.Data.Sigma @@ -23,6 +24,9 @@ open import Cubical.Categories.Monad.Base open import Cubical.Tactics.CategorySolver.Reflection open import Cubical.Tactics.FunctorSolver.Reflection + +open import Cubical.Foundations.Isomorphism.More + private variable ℓ ℓ' : Level @@ -77,15 +81,15 @@ module _ (C : Category ℓ ℓ') where open import Cubical.Categories.Adjoint.UniversalElements open import Cubical.Categories.Presheaf.Representable - open UnivElt - open isUniversal + open UniversalElement + open isEquiv F : LeftAdjoint _ _ G F c .vertex = c F c .element = η - F c .universal .coinduction = λ z → z - F c .universal .commutes ϕ = bind-l - F c .universal .is-uniq ϕ f p = sym bind-l ∙ p - + F c .universal d = isIsoToIsEquiv + ( (λ x → x) + , (λ b → bind-l) + , λ f → bind-l) -- TODO: by abstract nonsense construct a monad structure for T open ExtensionSystemFor diff --git a/Cubical/Categories/NaturalTransformation/More.agda b/Cubical/Categories/NaturalTransformation/More.agda index 29e86045..7727dbe5 100644 --- a/Cubical/Categories/NaturalTransformation/More.agda +++ b/Cubical/Categories/NaturalTransformation/More.agda @@ -13,6 +13,7 @@ open import Cubical.Categories.Commutativity open import Cubical.Categories.Morphism open import Cubical.Categories.Isomorphism open import Cubical.Categories.NaturalTransformation.Base +open import Cubical.Categories.NaturalTransformation.Properties open import Cubical.Categories.Instances.Functors @@ -58,29 +59,6 @@ _∘ʰ'_ = whiskerTrans' α⁻¹ = pathToNatTrans (sym F-assoc) 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 _ {F F' G G' : Functor C D} {α : NatIso F G} {β : NatIso F' G'} where open Functor makeNatIsoPathP : ∀ (p : F ≡ F') (q : G ≡ G') @@ -96,29 +74,6 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where (λ i → isPropIsIso (makeNatIsoPathP p q P i .trans .N-ob x)) (α .nIso _) (β .nIso _) i -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 - - - module _ {A : Category ℓA ℓA'} {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} diff --git a/Cubical/Categories/Presheaf/More.agda b/Cubical/Categories/Presheaf/More.agda index 289cd459..40a15a8a 100644 --- a/Cubical/Categories/Presheaf/More.agda +++ b/Cubical/Categories/Presheaf/More.agda @@ -2,6 +2,9 @@ module Cubical.Categories.Presheaf.More where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Structure open import Cubical.Categories.Category open import Cubical.Categories.Constructions.Lift @@ -9,6 +12,7 @@ open import Cubical.Categories.Instances.Sets open import Cubical.Categories.Instances.Functors open import Cubical.Categories.Functor.Base open import Cubical.Categories.Presheaf.Base +open import Cubical.Categories.Presheaf.Representable open import Cubical.Categories.Instances.Sets.More @@ -19,25 +23,6 @@ private variable ℓ ℓ' ℓS ℓS' : Level -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 [ C [ ϕ ∘ᴾ⟨ P ⟩ f ] ∘ᴾ⟨ P ⟩ g ] -∘ᴾAssoc C P ϕ f g i = P .F-seq f g i ϕ - -- Isomorphism between presheaves of different levels PshIso : (C : Category ℓ ℓ') (P : Presheaf C ℓS) @@ -54,3 +39,44 @@ IdPshIso C P = idCatIso 𝓟* : Category ℓ ℓ' → (ℓS : Level) → Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓS)) 𝓟* C ℓS = Functor C (SET ℓS) + +module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where + open UniversalElement + UniversalElementOn : C .ob → Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) + UniversalElementOn vertex = + Σ[ element ∈ (P ⟅ vertex ⟆) .fst ] isUniversal C P vertex element + + UniversalElementToUniversalElementOn : + (ue : UniversalElement C P) → UniversalElementOn (ue .vertex) + UniversalElementToUniversalElementOn ue .fst = ue .element + UniversalElementToUniversalElementOn ue .snd = ue .universal + +module UniversalElementNotation {ℓo}{ℓh} + {C : Category ℓo ℓh} {ℓp} {P : Presheaf C ℓp} (ue : UniversalElement C P) + where + open UniversalElement ue + + intro : ∀ {c} → ⟨ P ⟅ c ⟆ ⟩ → C [ c , vertex ] + intro p = universal _ .equiv-proof p .fst .fst + + β : ∀ {c} → {p : ⟨ P ⟅ c ⟆ ⟩} → (element ∘ᴾ⟨ C , P ⟩ intro p) ≡ p + β {p = p} = universal _ .equiv-proof p .fst .snd + + η : ∀ {c} → {f : C [ c , vertex ]} → f ≡ intro (element ∘ᴾ⟨ C , P ⟩ f) + η {f = f} = cong fst (sym (universal _ .equiv-proof (element ∘ᴾ⟨ C , P ⟩ f) + .snd (_ , refl))) + + weak-η : C .id ≡ intro element + weak-η = η ∙ cong intro (∘ᴾId C P _) + + extensionality : ∀ {c} → {f f' : C [ c , vertex ]} + → (element ∘ᴾ⟨ C , P ⟩ f) ≡ (element ∘ᴾ⟨ C , P ⟩ f') + → f ≡ f' + extensionality = isoFunInjective (equivToIso (_ , (universal _))) _ _ + + intro-natural : ∀ {c' c} → {p : ⟨ P ⟅ c ⟆ ⟩}{f : C [ c' , c ]} + → intro p ∘⟨ C ⟩ f ≡ intro (p ∘ᴾ⟨ C , P ⟩ f) + intro-natural = extensionality + ( (∘ᴾAssoc C P _ _ _ + ∙ cong (action C P _) β) + ∙ sym β) diff --git a/Cubical/Categories/Presheaf/Morphism.agda b/Cubical/Categories/Presheaf/Morphism.agda deleted file mode 100644 index 37950d67..00000000 --- a/Cubical/Categories/Presheaf/Morphism.agda +++ /dev/null @@ -1,93 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Categories.Presheaf.Morphism where - -open import Cubical.Foundations.Prelude -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.Isomorphism -open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Limits -open import Cubical.Categories.Presheaf.Base -open import Cubical.Data.Sigma - -open import Cubical.Categories.Constructions.Elements.More -open import Cubical.Categories.Instances.Sets.More -open import Cubical.Categories.Presheaf.More -open import Cubical.Categories.Presheaf.Representable -open import Cubical.Categories.Limits.Terminal.More - -{- - - 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. - - 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 UnivElt -open isUniversal - -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 - push-elt : Elementᴾ {C = C} P → Elementᴾ {C = D} Q - push-elt (A , η) = (F ⟅ A ⟆) , (h .N-ob A (lift η) .lower) - - push-eltNat : ∀ {B : C .ob} (η : Elementᴾ {C = C} P) (f : C [ B , η .fst ]) - → D [ push-elt η .snd ∘ᴾ⟨ Q ⟩ F .F-hom f ] - ≡ push-elt (B , C [ η .snd ∘ᴾ⟨ P ⟩ f ]) .snd - push-eltNat η f i = h .N-hom f (~ i) (lift (η .snd)) .lower - - push-eltF : Functor (∫ᴾ_ {C = C} P) (∫ᴾ_ {C = D} Q) - push-eltF .F-ob = push-elt - push-eltF .F-hom {x}{y} (f , commutes) = F .F-hom f , sym ( - D [ push-elt _ .snd ∘ᴾ⟨ Q ⟩ F .F-hom f ] - ≡⟨ push-eltNat y f ⟩ - push-elt (_ , C [ y .snd ∘ᴾ⟨ P ⟩ f ]) .snd - ≡⟨ cong (λ a → push-elt a .snd) (ΣPathP (refl , (sym commutes))) ⟩ - push-elt x .snd ∎) - push-eltF .F-id = Σ≡Prop (λ x → (Q ⟅ _ ⟆) .snd _ _) (F .F-id) - push-eltF .F-seq f g = - Σ≡Prop ((λ x → (Q ⟅ _ ⟆) .snd _ _)) (F .F-seq (f .fst) (g .fst)) - - preserves-representation : ∀ (η : UnivElt C P) → - Type (ℓ-max (ℓ-max ℓd ℓd') ℓq) - preserves-representation η = isUniversal D Q (push-elt (elementᴾ _ _ η)) - - preserves-representability : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max - (ℓ-max ℓc ℓc') ℓd) ℓd') ℓp) ℓq) - preserves-representability = ∀ η → preserves-representation η - - -- What is the nice HoTT formulation of this? - preserve-represention→preserves-representability : - ∀ η → preserves-representation η → preserves-representability - preserve-represention→preserves-representability η preserves-η η' = - isTerminalElement→isUniversal D Q - (preserveOnePreservesAll (∫ᴾ_ {C = C} P) - (∫ᴾ_ {C = D} Q) - push-eltF - (UnivElt→UniversalElement C P η) - (isUniversal→isTerminalElement D Q preserves-η) - (UnivElt→UniversalElement C P η')) diff --git a/Cubical/Categories/Presheaf/Representable.agda b/Cubical/Categories/Presheaf/Representable.agda deleted file mode 100644 index 866cd74c..00000000 --- a/Cubical/Categories/Presheaf/Representable.agda +++ /dev/null @@ -1,296 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Categories.Presheaf.Representable where - -open import Cubical.Data.Sigma -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Prelude -open import Cubical.Categories.Category -open import Cubical.Categories.Yoneda -open import Cubical.Categories.Constructions.Elements -open import Cubical.Categories.Functor -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Instances.Functors -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.HITs.PropositionalTruncation.Base - -open import Cubical.Categories.Constructions.Elements.More -open import Cubical.Categories.Presheaf.More -open import Cubical.Categories.Yoneda.More - -private - variable ℓ ℓ' : Level - -open Category -open Contravariant - --- | 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 ℓh) ℓp) - Representation = - Σ[ A ∈ C .ob ] PshIso C (C [-, A ]) P - - Representable : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) - Representable = ∥ Representation ∥₁ - - Elements = ∫ᴾ_ {C = C} P - -- | By the Yoneda lemma, the data of a representation is equivalent - -- | to just specifying a universal element of the presheaf - UniversalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) - UniversalElement = Terminal Elements - - hasUniversalElement : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) - hasUniversalElement = ∥ UniversalElement ∥₁ - - -- A packaged record version that is easier to use - record isUniversal - (η : Elementᴾ {C = C} P) : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) where - private - vertex = η .fst - element = η .snd - field - coinduction : ∀ {b} → (P ⟅ b ⟆) .fst → C [ b , vertex ] - commutes : ∀ {b} (ϕ : (P ⟅ b ⟆) .fst) → - C [ element ∘ᴾ⟨ P ⟩ coinduction ϕ ] ≡ ϕ - is-uniq : ∀ {b} (ϕ : (P ⟅ b ⟆) .fst) f → - (C [ element ∘ᴾ⟨ P ⟩ f ] ≡ ϕ) → f ≡ coinduction ϕ - - determined-by-elt : ∀ {b} - → {f g : C [ b , vertex ]} - → C [ element ∘ᴾ⟨ P ⟩ f ] ≡ C [ element ∘ᴾ⟨ P ⟩ g ] - → f ≡ g - determined-by-elt {f = f}{g} ef≡eg = - f - ≡⟨ is-uniq (C [ element ∘ᴾ⟨ P ⟩ f ]) f refl ⟩ - coinduction (C [ element ∘ᴾ⟨ P ⟩ f ]) - ≡[ i ]⟨ coinduction (ef≡eg i) ⟩ - coinduction (C [ element ∘ᴾ⟨ P ⟩ g ]) - ≡⟨ sym (is-uniq ((C [ element ∘ᴾ⟨ P ⟩ g ])) g refl) ⟩ - g ∎ - - η-expansion : ∀ {b} (f : C [ b , vertex ]) → - f ≡ coinduction (C [ element ∘ᴾ⟨ P ⟩ f ]) - η-expansion f = is-uniq (C [ element ∘ᴾ⟨ P ⟩ f ]) f refl - - coinduction-elt : C .id ≡ coinduction element - coinduction-elt = is-uniq element (C .id) (∘ᴾId C P _) - - is-uniq-converse : ∀ {b} (ϕ : (P ⟅ b ⟆) .fst) f → - f ≡ coinduction ϕ → C [ element ∘ᴾ⟨ P ⟩ f ] ≡ ϕ - is-uniq-converse ϕ f p = - C [ element ∘ᴾ⟨ P ⟩ f ] - ≡[ i ]⟨ C [ element ∘ᴾ⟨ P ⟩ p i ] ⟩ - C [ element ∘ᴾ⟨ P ⟩ coinduction ϕ ] - ≡⟨ commutes ϕ ⟩ - ϕ ∎ - - coinduction-natural : ∀ {a b} → (ϕ : (P ⟅ b ⟆) .fst) → (f : C [ a , b ]) - → coinduction ϕ ∘⟨ C ⟩ f ≡ - coinduction (C [ ϕ ∘ᴾ⟨ P ⟩ f ]) - coinduction-natural ϕ f = - is-uniq (C [ ϕ ∘ᴾ⟨ P ⟩ f ]) (coinduction ϕ ∘⟨ C ⟩ f) - (C [ element ∘ᴾ⟨ P ⟩ (coinduction ϕ ∘⟨ C ⟩ f) ] - ≡⟨ ∘ᴾAssoc C P element (coinduction ϕ) f ⟩ - C [ C [ element ∘ᴾ⟨ P ⟩ coinduction ϕ ] ∘ᴾ⟨ P ⟩ f ] - ≡[ i ]⟨ C [ commutes ϕ i ∘ᴾ⟨ P ⟩ f ] ⟩ - C [ ϕ ∘ᴾ⟨ P ⟩ f ] ∎) - - record UnivElt : Type (ℓ-max (ℓ-max ℓo ℓh) ℓp) where - field - vertex : C .ob - element : (P ⟅ vertex ⟆) .fst - universal : isUniversal (vertex , element) - - open UnivElt - open isUniversal - - elementᴾ : UnivElt → Elementᴾ {C = C} P - elementᴾ η = (η .vertex , η .element) - - private - univEltMor : ∀ η {η' : Elementᴾ {C = C} P} → - (η'-univ : isUniversal η') → - C [ η .fst , η' .fst ] - univEltMor η η'-univ = η'-univ .coinduction (η .snd) - - univEltLemma : ∀ {η η' : Elementᴾ {C = C} P} → (η-univ : isUniversal η) → - (η'-univ : isUniversal η') → - univEltMor η η'-univ ∘⟨ C ⟩ univEltMor η' η-univ ≡ C .id - univEltLemma {η}{η'} η-univ η'-univ = - η'-univ .coinduction (η .snd) ∘⟨ C ⟩ η-univ .coinduction (η' .snd) - ≡⟨ η'-univ .is-uniq (η' .snd) _ lem ⟩ - η'-univ .coinduction (η' .snd) - ≡⟨ sym (η'-univ .is-uniq _ (C .id) (∘ᴾId C P (η' .snd))) ⟩ - C .id ∎ where - - lem : (C [ η' .snd ∘ᴾ⟨ P ⟩ η'-univ .coinduction (η .snd) ∘⟨ C ⟩ - η-univ .coinduction (η' .snd) ]) ≡ η' .snd - lem = - (C [ η' .snd ∘ᴾ⟨ P ⟩ η'-univ .coinduction (η .snd) ∘⟨ C ⟩ - η-univ .coinduction (η' .snd) ]) - ≡⟨ ∘ᴾAssoc C P _ _ _ ⟩ - (C [ C [ η' .snd ∘ᴾ⟨ P ⟩ η'-univ .coinduction (η .snd) ] ∘ᴾ⟨ P ⟩ - η-univ .coinduction (η' .snd) ]) - ≡[ i ]⟨ C [ η'-univ .commutes (η .snd) i ∘ᴾ⟨ P ⟩ - η-univ .coinduction (η' .snd) ] ⟩ - (C [ η .snd ∘ᴾ⟨ P ⟩ η-univ .coinduction (η' .snd) ]) - ≡⟨ η-univ .commutes _ ⟩ - η' .snd ∎ - - univEltIso : ∀ {η η' : Elementᴾ {C = C} P} → isUniversal η → isUniversal η' - → CatIso C (η .fst) (η' .fst) - univEltIso {η}{η'} η-univ η'-univ .fst = univEltMor η η'-univ - univEltIso {η}{η'} η-univ η'-univ .snd .isIso.inv = univEltMor η' η-univ - univEltIso {η}{η'} η-univ η'-univ .snd .isIso.sec = - univEltLemma η-univ η'-univ - univEltIso {η}{η'} η-univ η'-univ .snd .isIso.ret = - univEltLemma η'-univ η-univ - - -- First the logical equivalence - isTerminalElement→isUniversal : ∀ {η : Elementᴾ {C = C} P} → - isTerminal Elements η → isUniversal η - isTerminalElement→isUniversal {η} term .coinduction ϕ = term (_ , ϕ) .fst .fst - isTerminalElement→isUniversal term .commutes ϕ = sym (term (_ , ϕ) .fst .snd) - isTerminalElement→isUniversal term .is-uniq ϕ f commutes i = - term (_ , ϕ) .snd (f , sym commutes) (~ i) .fst - - isUniversal→isTerminalElement : ∀ {η : Elementᴾ {C = C} P} → - isUniversal η → isTerminal Elements η - isUniversal→isTerminalElement η-univ ϕ .fst .fst = - η-univ .coinduction (ϕ .snd) - isUniversal→isTerminalElement η-univ ϕ .fst .snd = - sym (η-univ .commutes (ϕ .snd)) - isUniversal→isTerminalElement η-univ ϕ .snd f = - Σ≡Prop (λ x → (P ⟅ _ ⟆) .snd _ _) - (sym (η-univ .is-uniq (ϕ .snd) (f .fst) (sym (f .snd)))) - - isPropIsUniversal : ∀ η → isProp (isUniversal η) - isPropIsUniversal η = - isPropRetract isUniversal→isTerminalElement - isTerminalElement→isUniversal - reason - (isPropIsTerminal Elements η) where - reason : (x : isUniversal (η .fst , η .snd)) - → isTerminalElement→isUniversal (isUniversal→isTerminalElement x) ≡ x - reason η-univ i .coinduction ϕ = η-univ .coinduction ϕ - reason η-univ i .commutes ϕ = η-univ .commutes ϕ - reason η-univ i .is-uniq ϕ f commutes = η-univ .is-uniq ϕ f commutes - - UniversalElement→UnivElt : UniversalElement → UnivElt - UniversalElement→UnivElt η .vertex = η .fst .fst - UniversalElement→UnivElt η .element = η .fst .snd - UniversalElement→UnivElt η .universal = isTerminalElement→isUniversal (η .snd) - - UnivElt→UniversalElement : UnivElt → UniversalElement - UnivElt→UniversalElement η .fst .fst = η .vertex - UnivElt→UniversalElement η .fst .snd = η .element - UnivElt→UniversalElement η .snd = isUniversal→isTerminalElement (η .universal) - - UniversalElement≅UnivElt : Iso UniversalElement UnivElt - UniversalElement≅UnivElt .Iso.fun = UniversalElement→UnivElt - UniversalElement≅UnivElt .Iso.inv = UnivElt→UniversalElement - UniversalElement≅UnivElt .Iso.rightInv η = refl - UniversalElement≅UnivElt .Iso.leftInv η = - Σ≡Prop (isPropIsTerminal Elements) refl - - open NatTrans - isTerminalElement→YoIso : (η : Terminal Elements) - → Cubical.Categories.Category.isIso - (PresheafCategory C (ℓ-max ℓh ℓp)) - (Iso.inv (yonedaᴾ* {C = C} P (η .fst .fst)) (η .fst .snd)) - isTerminalElement→YoIso ((A , η) , η-univ) = - FUNCTORIso (C ^op) (SET (ℓ-max ℓh ℓp)) _ pointwise where - pointwise : ∀ c → Cubical.Categories.Category.isIso - (SET (ℓ-max ℓh ℓp)) - (Iso.inv (yonedaᴾ* {C = C} P A) η ⟦ c ⟧) - pointwise c .isIso.inv ϕ = lift (η-univ (_ , ϕ .lower) .fst .fst) - pointwise c .isIso.sec = - funExt (λ ϕ i → lift (η-univ (_ , ϕ .lower) .fst .snd (~ i))) - pointwise c .isIso.ret = - funExt (λ f i → - lift ( - η-univ (_ , C [ η ∘ᴾ⟨ P ⟩ f .lower ]) .snd (f .lower , refl) i .fst)) - - YoIso→isTerminalElement : ∀ A - → (i : PshIso C (C [-, A ]) P) - → isTerminal Elements - (A , (i .fst .N-ob A (lift (C .id)) .lower)) - YoIso→isTerminalElement A (YoA→P , isiso P→YoA sec ret) (B , ϕ) .fst .fst = - P→YoA .N-ob B (lift ϕ) .lower - YoIso→isTerminalElement A (YoA→P , isiso P→YoA sec ret) (B , ϕ) .fst .snd = - ϕ - ≡[ i ]⟨ (sec (~ i) .N-ob B (lift ϕ)) .lower ⟩ - YoA→P .N-ob B (P→YoA .N-ob B (lift ϕ)) .lower - ≡[ i ]⟨ YoA→P .N-ob B - (lift (C .⋆IdR (P→YoA .N-ob B (lift ϕ) .lower) (~ i))) .lower ⟩ - (YoA→P .N-ob B (lift (C .id ∘⟨ C ⟩ P→YoA .N-ob B (lift ϕ) .lower))) .lower - ≡[ i ]⟨ YoA→P .N-hom (P→YoA .N-ob B - (lift ϕ) .lower) i (lift (C .id)) .lower ⟩ - C [ YoA→P .N-ob A (lift (C .id)) .lower ∘ᴾ⟨ P ⟩ - P→YoA .N-ob B (lift ϕ) .lower ] ∎ - YoIso→isTerminalElement A (YoA→P , isiso P→YoA sec ret) (B , ϕ) - .snd f+ @ (f , ϕ=η∘f) = - ∫ᴾhomEqSimpl {C = C} P ((P→YoA .N-ob B (lift ϕ) .lower) , _) f+ - (P→YoA .N-ob B (lift ϕ) .lower - ≡[ i ]⟨ P→YoA .N-ob B (lift (ϕ=η∘f i)) .lower ⟩ - P→YoA .N-ob B - (lift (C [ YoA→P .N-ob A (lift (C .id)) .lower ∘ᴾ⟨ P ⟩ f ])) .lower - ≡[ i ]⟨ P→YoA .N-hom f i (YoA→P .N-ob A (lift (C .id))) .lower ⟩ - P→YoA .N-ob A (YoA→P .N-ob A (lift (C .id))) .lower ∘⟨ C ⟩ f - ≡[ i ]⟨ ret i .N-ob A (lift (C .id)) .lower ∘⟨ C ⟩ f ⟩ - C .id ∘⟨ C ⟩ f - ≡⟨ C .⋆IdR f ⟩ - f ∎) - - RepresentationToUniversalElement : Representation → UniversalElement - RepresentationToUniversalElement (A , YoA→P , YoA→P-isIso) .fst .fst = A - RepresentationToUniversalElement (A , YoA→P , YoA→P-isIso) .fst .snd = - Iso.fun (yonedaᴾ* P A) YoA→P - RepresentationToUniversalElement (A , YoA→P , YoA→P-isIso) .snd = - YoIso→isTerminalElement A (YoA→P , YoA→P-isIso) - - UniversalElementToRepresentation : UniversalElement → Representation - UniversalElementToRepresentation ((A , η) , η-univ) .fst = A - UniversalElementToRepresentation η-terminal @ ((A , η) , η-univ) .snd = - (Iso.inv (yonedaᴾ* P A) η) , isTerminalElement→YoIso η-terminal - - Representation≅UniversalElement : Iso Representation UniversalElement - Representation≅UniversalElement .Iso.fun = RepresentationToUniversalElement - Representation≅UniversalElement .Iso.inv = UniversalElementToRepresentation - Representation≅UniversalElement .Iso.rightInv ((A , η) , _) = - Σ≡Prop (isPropIsTerminal Elements) - (ΣPathP (refl , yonedaᴾ* {C = C} P A .rightInv η)) - where open Iso - Representation≅UniversalElement .Iso.leftInv (A , YoA→P , _) = - ΣPathP (refl , (Σ≡Prop isPropIsIso (yonedaᴾ* {C = C} P A .leftInv YoA→P))) - where open Iso - - Representation≅UnivElt : Iso Representation UnivElt - Representation≅UnivElt = - compIso Representation≅UniversalElement UniversalElement≅UnivElt - - RepresentationToUnivElt : Representation → UnivElt - RepresentationToUnivElt = Iso.fun Representation≅UnivElt - - UnivEltToRepresentation : UnivElt → Representation - UnivEltToRepresentation = Iso.inv Representation≅UnivElt - - -- If A and B both represent P then A ≅ B - sameUMP→CatIso : (u : UnivElt) → (v : UnivElt) → - CatIso C (u .vertex) (v .vertex) - sameUMP→CatIso u v = - preserveIsosF {F = domain {C = C} P} - (terminalToIso (∫ᴾ_ {C = C} P) - (UnivElt→UniversalElement u) - (UnivElt→UniversalElement v)) - -selfRepresents : (C : Category ℓ ℓ') → (A : C .ob) → - Representation C (C [-, A ]) -selfRepresents C A = A , IdPshIso C (C [-, A ]) diff --git a/Cubical/Categories/Profunctor/Equivalence.agda b/Cubical/Categories/Profunctor/Equivalence.agda index c297a835..5935873c 100644 --- a/Cubical/Categories/Profunctor/Equivalence.agda +++ b/Cubical/Categories/Profunctor/Equivalence.agda @@ -3,351 +3,350 @@ -} {-# OPTIONS --safe #-} --- module Cubical.Categories.Profunctor.Equivalence where module Cubical.Categories.Profunctor.Equivalence where -open import Cubical.Categories.Profunctor.General +-- open import Cubical.Categories.Profunctor.General -open import Cubical.Reflection.RecordEquiv +-- open import Cubical.Reflection.RecordEquiv -open import Cubical.Foundations.Prelude hiding (Path) -open import Cubical.Foundations.Structure -open import Cubical.Foundations.Path -open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) -open import Cubical.Foundations.Isomorphism +-- open import Cubical.Foundations.Prelude hiding (Path) +-- open import Cubical.Foundations.Structure +-- open import Cubical.Foundations.Path +-- open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) +-- open import Cubical.Foundations.Isomorphism -open import Cubical.Data.Graph.Base -open import Cubical.Data.Graph.Path -open import Cubical.Data.Sigma.Properties +-- open import Cubical.Data.Graph.Base +-- open import Cubical.Data.Graph.Path +-- open import Cubical.Data.Sigma.Properties -open import Cubical.Categories.Category -open import Cubical.Categories.Functor -open import Cubical.Categories.Bifunctor.Base -open import Cubical.Categories.Instances.Functors -open import Cubical.Categories.NaturalTransformation -open import Cubical.Categories.Constructions.BinProduct -open import Cubical.Categories.Constructions.Elements -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Functors.Constant -open import Cubical.Categories.Functors.HomFunctor -open import Cubical.Categories.Limits.Terminal +-- open import Cubical.Categories.Category +-- open import Cubical.Categories.Functor +-- open import Cubical.Categories.Bifunctor.Base +-- open import Cubical.Categories.Instances.Functors +-- open import Cubical.Categories.NaturalTransformation +-- open import Cubical.Categories.Constructions.BinProduct +-- open import Cubical.Categories.Constructions.Elements +-- open import Cubical.Categories.Instances.Sets +-- open import Cubical.Categories.Functors.Constant +-- open import Cubical.Categories.Functors.HomFunctor +-- open import Cubical.Categories.Limits.Terminal -open import Cubical.Categories.Presheaf.Representable -open import Cubical.Categories.Instances.Sets.More -open import Cubical.Categories.Instances.Functors.More -open import Cubical.Categories.NaturalTransformation.More -open import Cubical.Categories.Presheaf.More +-- open import Cubical.Categories.Presheaf.Representable +-- open import Cubical.Categories.Instances.Sets.More +-- open import Cubical.Categories.Instances.Functors.More +-- open import Cubical.Categories.NaturalTransformation.More +-- open import Cubical.Categories.Presheaf.More -open import Cubical.Tactics.CategorySolver.Reflection -open import Cubical.Tactics.FunctorSolver.Reflection +-- open import Cubical.Tactics.CategorySolver.Reflection +-- open import Cubical.Tactics.FunctorSolver.Reflection -private - variable ℓC ℓC' ℓD ℓD' ℓS : Level +-- private +-- variable ℓC ℓC' ℓD ℓD' ℓS : Level -module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') (R : C *-[ ℓS ]-o D) where +-- module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') (R : C *-[ ℓS ]-o D) where - open Category - open NatIso - open NatTrans - open Functor - open Contravariant - open Iso - open ProfHomo - open UnivElt - open isUniversal - open Bifunctor +-- open Category +-- open NatIso +-- open NatTrans +-- open Functor +-- open Contravariant +-- open Iso +-- open ProfHomo +-- open UnivElt +-- open isUniversal +-- open Bifunctor - ProfRepresentation≅PshFunctorRepresentation : Iso (ProfRepresentation C D R) - (PshFunctorRepresentation C D R) - ProfRepresentation≅PshFunctorRepresentation = - record { - fun = (ProfRepresentation→PshFunctorRepresentation C D R) ; - inv = (PshFunctorRepresentation→ProfRepresentation C D R) ; - rightInv = Psh→Prof→Psh ; - leftInv = Prof→Psh→Prof - } - where - Psh→Prof→Psh : (Psh : PshFunctorRepresentation C D R) - → (ProfRepresentation→PshFunctorRepresentation C D R) - ((PshFunctorRepresentation→ProfRepresentation C D R) Psh) - ≡ Psh - Psh→Prof→Psh (G , η) = - ΣPathP ( - refl , - makeNatIsoPathP - refl - refl - (funExt (λ c → makeNatTransPath (funExt (λ d → refl)))) - ) +-- ProfRepresentation≅PshFunctorRepresentation : Iso (ProfRepresentation C D R) +-- (PshFunctorRepresentation C D R) +-- ProfRepresentation≅PshFunctorRepresentation = +-- record { +-- fun = (ProfRepresentation→PshFunctorRepresentation C D R) ; +-- inv = (PshFunctorRepresentation→ProfRepresentation C D R) ; +-- rightInv = Psh→Prof→Psh ; +-- leftInv = Prof→Psh→Prof +-- } +-- where +-- Psh→Prof→Psh : (Psh : PshFunctorRepresentation C D R) +-- → (ProfRepresentation→PshFunctorRepresentation C D R) +-- ((PshFunctorRepresentation→ProfRepresentation C D R) Psh) +-- ≡ Psh +-- Psh→Prof→Psh (G , η) = +-- ΣPathP ( +-- refl , +-- makeNatIsoPathP +-- refl +-- refl +-- (funExt (λ c → makeNatTransPath (funExt (λ d → refl)))) +-- ) - Prof→Psh→Prof : (Prof : ProfRepresentation C D R) - → (PshFunctorRepresentation→ProfRepresentation C D R) - ((ProfRepresentation→PshFunctorRepresentation C D R) Prof) - ≡ Prof - Prof→Psh→Prof (G , η) = - let - (G' , η') = (PshFunctorRepresentation→ProfRepresentation C D R) - (ProfRepresentation→PshFunctorRepresentation C D R (G , η)) - R' = (Functor→Prof*-o C D - (fst (PshFunctorRepresentation→ProfRepresentation C D R - (ProfRepresentation→PshFunctorRepresentation C D R (G , η))))) - in - ΣPathP ( - refl , - ΣPathP ( - cong′ - (λ X → isoProfHomoProfHomo' R R' .inv (ProfHomo'IsoΣ R R' .inv X)) - -- Turn the records into Σ types, then prove we have a path between - -- the Σ-tized versions of η and η' - (ΣPathP - (refl , - (ΣPathP ( - (isProp-natL R R' - (isoProfHomoProfHomo' R R' .fun (η .fst)) - (ProfHomo'.PH-natL (isoProfHomoProfHomo' R R' .fun (η' .fst))) - (λ c c' d f r i → PH-natL (fst η) f r i) - ) , - (isProp-natR R R' - ((isoProfHomoProfHomo' R R' .fun (η .fst))) - ((ProfHomo'.PH-natR (isoProfHomoProfHomo' R R' - .fun (η' .fst)))) - (λ c d d' r g i → PH-natR (fst η) r g i) - ) - )) - ) - ) , - funExt (λ d → funExt (λ c → refl)) - ) - ) +-- Prof→Psh→Prof : (Prof : ProfRepresentation C D R) +-- → (PshFunctorRepresentation→ProfRepresentation C D R) +-- ((ProfRepresentation→PshFunctorRepresentation C D R) Prof) +-- ≡ Prof +-- Prof→Psh→Prof (G , η) = +-- let +-- (G' , η') = (PshFunctorRepresentation→ProfRepresentation C D R) +-- (ProfRepresentation→PshFunctorRepresentation C D R (G , η)) +-- R' = (Functor→Prof*-o C D +-- (fst (PshFunctorRepresentation→ProfRepresentation C D R +-- (ProfRepresentation→PshFunctorRepresentation C D R (G , η))))) +-- in +-- ΣPathP ( +-- refl , +-- ΣPathP ( +-- cong′ +-- (λ X → isoProfHomoProfHomo' R R' .inv (ProfHomo'IsoΣ R R' .inv X)) +-- -- Turn the records into Σ types, then prove we have a path between +-- -- the Σ-tized versions of η and η' +-- (ΣPathP +-- (refl , +-- (ΣPathP ( +-- (isProp-natL R R' +-- (isoProfHomoProfHomo' R R' .fun (η .fst)) +-- (ProfHomo'.PH-natL (isoProfHomoProfHomo' R R' .fun (η' .fst))) +-- (λ c c' d f r i → PH-natL (fst η) f r i) +-- ) , +-- (isProp-natR R R' +-- ((isoProfHomoProfHomo' R R' .fun (η .fst))) +-- ((ProfHomo'.PH-natR (isoProfHomoProfHomo' R R' +-- .fun (η' .fst)))) +-- (λ c d d' r g i → PH-natR (fst η) r g i) +-- ) +-- )) +-- ) +-- ) , +-- funExt (λ d → funExt (λ c → refl)) +-- ) +-- ) - PshFunctorRepresentation≅ParamUnivElt : Iso (PshFunctorRepresentation C D R) - (ParamUnivElt C D R) - PshFunctorRepresentation≅ParamUnivElt = - record { - fun = PshFunctorRepresentation→ParamUnivElt C D R ; - inv = ParamUnivElt→PshFunctorRepresentation C D R ; - rightInv = Univ→PshFunctor→Univ ; - leftInv = PshFunctor→Univ→PshFunctor - } - where - Univ→PshFunctor→Univ : ∀ (U : ParamUnivElt C D R) → - ((PshFunctorRepresentation→ParamUnivElt C D R) - ((ParamUnivElt→PshFunctorRepresentation C D R) U) ≡ - U) - Univ→PshFunctor→Univ U = - let (G , η) = (ParamUnivElt→PshFunctorRepresentation C D R) U - U' = PshFunctorRepresentation→ParamUnivElt C D R (G , η) - in - funExt (λ c → - -- easier to do proof with UniversalElements, use isomorphism - sym (UniversalElement≅UnivElt D (pAppR R c) .Iso.rightInv (U' c)) - ∙ - congS (UniversalElement→UnivElt D (pAppR R c)) - -- underlying proof of Universal Elements being the same - -- terminal object - ( ΣPathPProp - {u = UnivElt→UniversalElement D (pAppR R c) (U' c)} - {v = UnivElt→UniversalElement D (pAppR R c) (U c)} - (isPropIsTerminal (∫ᴾ_ {C = D} (pAppR R c))) - ( ΣPathP ( - -- same object - refl , - -- paths equal as εc ⋆ id = εc - (λ i → ((pAppR R c) .F-id (i)) (U c .element)) - )) - ) - ∙ - UniversalElement≅UnivElt D (pAppR R c) .Iso.rightInv (U c) - ) +-- PshFunctorRepresentation≅ParamUnivElt : Iso (PshFunctorRepresentation C D R) +-- (ParamUnivElt C D R) +-- PshFunctorRepresentation≅ParamUnivElt = +-- record { +-- fun = PshFunctorRepresentation→ParamUnivElt C D R ; +-- inv = ParamUnivElt→PshFunctorRepresentation C D R ; +-- rightInv = Univ→PshFunctor→Univ ; +-- leftInv = PshFunctor→Univ→PshFunctor +-- } +-- where +-- Univ→PshFunctor→Univ : ∀ (U : ParamUnivElt C D R) → +-- ((PshFunctorRepresentation→ParamUnivElt C D R) +-- ((ParamUnivElt→PshFunctorRepresentation C D R) U) ≡ +-- U) +-- Univ→PshFunctor→Univ U = +-- let (G , η) = (ParamUnivElt→PshFunctorRepresentation C D R) U +-- U' = PshFunctorRepresentation→ParamUnivElt C D R (G , η) +-- in +-- funExt (λ c → +-- -- easier to do proof with UniversalElements, use isomorphism +-- sym (UniversalElement≅UnivElt D (pAppR R c) .Iso.rightInv (U' c)) +-- ∙ +-- congS (UniversalElement→UnivElt D (pAppR R c)) +-- -- underlying proof of Universal Elements being the same +-- -- terminal object +-- ( ΣPathPProp +-- {u = UnivElt→UniversalElement D (pAppR R c) (U' c)} +-- {v = UnivElt→UniversalElement D (pAppR R c) (U c)} +-- (isPropIsTerminal (∫ᴾ_ {C = D} (pAppR R c))) +-- ( ΣPathP ( +-- -- same object +-- refl , +-- -- paths equal as εc ⋆ id = εc +-- (λ i → ((pAppR R c) .F-id (i)) (U c .element)) +-- )) +-- ) +-- ∙ +-- UniversalElement≅UnivElt D (pAppR R c) .Iso.rightInv (U c) +-- ) - PshFunctor→Univ→PshFunctor : ∀ (Psh : (PshFunctorRepresentation C D R)) → - ((ParamUnivElt→PshFunctorRepresentation C D R) - ((PshFunctorRepresentation→ParamUnivElt C D R) Psh) ≡ - Psh) - PshFunctor→Univ→PshFunctor (G , η) = - let η⁻¹ = symNatIso η - U' = ((PshFunctorRepresentation→ParamUnivElt C D R) (G , η)) - (G' , η') = ((ParamUnivElt→PshFunctorRepresentation C D R) U') - G'≡G = (Functor≡ - -- object map is same - (λ c → refl) - -- morphisms are the same due to the - -- uniqueness of coinduction - (λ {x} {y} ϕ → - let dx = U' x .vertex - εx = U' x .element - dy = U' y .vertex - εy = U' y .element - R⟅-,y⟆ = (pAppR R y) - R⟅dx,-⟆ = (pAppL R dx) - in - G' ⟪ ϕ ⟫ - ≡⟨ sym(U' y .universal .is-uniq - ((R⟅dx,-⟆ ⟪ ϕ ⟫) εx) - (G ⟪ ϕ ⟫) - {- - nested proof that G ⟪ ϕ ⟫ also satisfies this - coinduction - this works by the following diagram between - the presheafs R⟅-,a⟆ and D[-,Ga] - ηx - R⟅-,x⟆ ==> D[-,Gx] - λR(ϕ) ∥ ∥ (G(ϕ) ∘ -) - ⇓ ηy ⇓ - R⟅-,y⟆ ==> D[-,Gy] +-- PshFunctor→Univ→PshFunctor : ∀ (Psh : (PshFunctorRepresentation C D R)) → +-- ((ParamUnivElt→PshFunctorRepresentation C D R) +-- ((PshFunctorRepresentation→ParamUnivElt C D R) Psh) ≡ +-- Psh) +-- PshFunctor→Univ→PshFunctor (G , η) = +-- let η⁻¹ = symNatIso η +-- U' = ((PshFunctorRepresentation→ParamUnivElt C D R) (G , η)) +-- (G' , η') = ((ParamUnivElt→PshFunctorRepresentation C D R) U') +-- G'≡G = (Functor≡ +-- -- object map is same +-- (λ c → refl) +-- -- morphisms are the same due to the +-- -- uniqueness of coinduction +-- (λ {x} {y} ϕ → +-- let dx = U' x .vertex +-- εx = U' x .element +-- dy = U' y .vertex +-- εy = U' y .element +-- R⟅-,y⟆ = (pAppR R y) +-- R⟅dx,-⟆ = (pAppL R dx) +-- in +-- G' ⟪ ϕ ⟫ +-- ≡⟨ sym(U' y .universal .is-uniq +-- ((R⟅dx,-⟆ ⟪ ϕ ⟫) εx) +-- (G ⟪ ϕ ⟫) +-- {- +-- nested proof that G ⟪ ϕ ⟫ also satisfies this +-- coinduction +-- this works by the following diagram between +-- the presheafs R⟅-,a⟆ and D[-,Ga] +-- ηx +-- R⟅-,x⟆ ==> D[-,Gx] +-- λR(ϕ) ∥ ∥ (G(ϕ) ∘ -) +-- ⇓ ηy ⇓ +-- R⟅-,y⟆ ==> D[-,Gy] - These are presheafs D ^op ⟶ SET, and we consider - the slice of this diagram at G ⟅ x ⟆ - ηxᴳˣ - R⟅Gx,x⟆ --→ D[Gx,Gx] - λR(ϕ)ᴳˣ | | (G(ϕ) ∘ -) - ↓ ↓ - R⟅Gx,y⟆ --→ D[Gx,Gy] - ηyᴳˣ - Note that by construction, the η and G here define - the coinduction and εx ⋆ maps - (these are what form the NatIso) - Thus the equality of the 2 expressions below follows - from the fact that η is a natural transformation +-- These are presheafs D ^op ⟶ SET, and we consider +-- the slice of this diagram at G ⟅ x ⟆ +-- ηxᴳˣ +-- R⟅Gx,x⟆ --→ D[Gx,Gx] +-- λR(ϕ)ᴳˣ | | (G(ϕ) ∘ -) +-- ↓ ↓ +-- R⟅Gx,y⟆ --→ D[Gx,Gy] +-- ηyᴳˣ +-- Note that by construction, the η and G here define +-- the coinduction and εx ⋆ maps +-- (these are what form the NatIso) +-- Thus the equality of the 2 expressions below follows +-- from the fact that η is a natural transformation - εx ⋆ - D[Gx,Gx] ---→ R⟅Gx,x⟆ - | id ⊢→ εx | - (G(ϕ) ∘ -) | ↓ ↓ | λR(ϕ)ᴳˣ = R⟅Gx,-⟆ ⟪ ϕ ⟫ - ↓ G(ϕ) ⊢→ ∎ ↓ - D[Gx,Gy] --→ R⟅Gx,y⟆ - εy ⋆ - -} - ( - (D [ εy ∘ᴾ⟨ R⟅-,y⟆ ⟩ (G ⟪ ϕ ⟫) ]) - ≡⟨ refl ⟩ - lower (((LiftF ∘F R⟅-,y⟆) ⟪ G ⟪ ϕ ⟫ ⟫) - ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ y ⟆)) (lift (D .id)))) - ≡⟨ (λ i → lower (((LiftF ∘Fb R ) .Bif-idR (~ i)) - (((LiftF ∘Fb R) .Bif-homL (G ⟪ ϕ ⟫) _) - ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ y ⟆)) - (lift (D .id)))))) ⟩ - lower ((((Prof*-o→Functor C D (LiftF ∘Fb R )) ⟅ y ⟆) - ⟪ G ⟪ ϕ ⟫ ⟫) ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ y ⟆)) - (lift (D .id)))) - -- since εy is defined in terms of R(Gy, y), we - -- first use naturality - -- to consider the relevant component of the εy ⋆ - -- map, namely the component at Gx - ≡⟨ (λ i → lower (((η⁻¹ .trans .N-ob y - .N-hom (G ⟪ ϕ ⟫)) (~ i)) (lift (D .id)) ) ) ⟩ - -- next, we use some recombining of G ϕ to see - -- it as an application - -- of a different Hom Functor applied to id at - -- Gx instead of Gy: - lower ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ x ⟆)) - (((Bifunctor→Functor (LiftF ∘Fb (HomBif D))) - ⟪ G ⟪ ϕ ⟫ , G ⟪ C .id ⟫ ⟫) (lift (D .id)))) - ≡⟨ (λ i → lower ((η⁻¹ .trans - .N-ob y .N-ob (G ⟅ x ⟆)) - (lift (((Bifunctor→Functor (HomBif D)) - ⟪ G ⟪ ϕ ⟫ , G .F-id i ⟫) (D .id)))) - )⟩ - lower ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ x ⟆)) - (lift (((Bifunctor→Functor (HomBif D)) ⟪ G ⟪ ϕ ⟫ , - D .id ⟫) (D .id)))) - ≡⟨ (λ i → lower ((η⁻¹ .trans .N-ob y .N-ob - (G ⟅ x ⟆)) (lift (((HomBif D) .Bif-idR (i) ∘f - (HomBif D) ⟪ G ⟪ ϕ ⟫ ⟫l ) (D .id))))) ⟩ - lower ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ x ⟆)) - (lift (G ⟪ ϕ ⟫ ⋆⟨ D ⟩ D .id))) - ≡⟨ (λ i → lower ((η⁻¹ .trans .N-ob y .N-ob - (G ⟅ x ⟆)) (lift (D .⋆IdL (D .⋆IdR (G ⟪ ϕ ⟫) - (i)) (~ i))))) ⟩ - lower (((η⁻¹ .trans .N-ob y) .N-ob (G ⟅ x ⟆)) - (lift ((D .id) ⋆⟨ D ⟩ G ⟪ ϕ ⟫))) - ≡⟨ (λ i → lower ( - ((η⁻¹ .trans .N-ob y) .N-ob (G ⟅ x ⟆)) - (lift (((HomBif D) ⟪ G ⟪ ϕ ⟫ ⟫r ∘f - ((HomBif D) .Bif-idL (~ i))) (D .id))) - )) ⟩ - lower ( - ((η⁻¹ .trans .N-ob y) .N-ob (G ⟅ x ⟆)) - (lift (((Bifunctor→Functor (HomBif D)) - ⟪ D .id , G ⟪ ϕ ⟫ ⟫) (D .id))) - ) - ≡⟨ refl ⟩ - lower ( - ((((Prof*-o→Functor C D (LiftF ∘Fb - (Functor→Prof*-o C D G))) ⟪ ϕ ⟫) - ⋆⟨ FUNCTOR (D ^op) (SET _) ⟩ - η⁻¹ .trans .N-ob y) .N-ob (G ⟅ x ⟆)) - (lift (D .id)) - ) - -- now, since we are operating of the section of Gx - -- as described above, we - -- can use the above argument to port over to εx - ≡⟨ (λ i → lower ( - (((η⁻¹ .trans .N-hom ϕ) (i)) .N-ob (G ⟅ x ⟆)) - (lift (D .id)) - )) ⟩ - lower ( - ((η⁻¹ .trans .N-ob x - ⋆⟨ FUNCTOR (D ^op) (SET _) ⟩ - ((Prof*-o→Functor C D (LiftF ∘Fb R)) ⟪ ϕ ⟫) - ) .N-ob (G ⟅ x ⟆)) - (lift (D .id)) - ) - ≡⟨ (λ i → (R .Bif-assoc (D .id) ϕ (i)) εx) ⟩ - (R .Bif-homL (D .id) _) ((R .Bif-homR (G ⟅ x ⟆) ϕ) εx) - ≡⟨ ( λ i → (R .Bif-idL i) - ((R .Bif-homR (G ⟅ x ⟆) ϕ) εx))⟩ - ((R⟅dx,-⟆ ⟪ ϕ ⟫) εx) ∎ - ) - )⟩ - G ⟪ ϕ ⟫ ∎) - ) - in ΣPathP ( - G'≡G , - (makeNatIsoPathP - refl - (cong′ (λ X → Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb - Functor→Prof*-o C D X)) G'≡G) - (funExt (λ (c : C .ob) → - (makeNatTransPathP - refl - (cong′ (λ X → (Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb - Functor→Prof*-o C D X)) .F-ob c) G'≡G) - (funExt (λ (d : D .ob) → - (funExt λ _ → refl) - )) - ) - )) - ) - ) +-- εx ⋆ +-- D[Gx,Gx] ---→ R⟅Gx,x⟆ +-- | id ⊢→ εx | +-- (G(ϕ) ∘ -) | ↓ ↓ | λR(ϕ)ᴳˣ = R⟅Gx,-⟆ ⟪ ϕ ⟫ +-- ↓ G(ϕ) ⊢→ ∎ ↓ +-- D[Gx,Gy] --→ R⟅Gx,y⟆ +-- εy ⋆ +-- -} +-- ( +-- (D [ εy ∘ᴾ⟨ R⟅-,y⟆ ⟩ (G ⟪ ϕ ⟫) ]) +-- ≡⟨ refl ⟩ +-- lower (((LiftF ∘F R⟅-,y⟆) ⟪ G ⟪ ϕ ⟫ ⟫) +-- ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ y ⟆)) (lift (D .id)))) +-- ≡⟨ (λ i → lower (((LiftF ∘Fb R ) .Bif-idR (~ i)) +-- (((LiftF ∘Fb R) .Bif-homL (G ⟪ ϕ ⟫) _) +-- ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ y ⟆)) +-- (lift (D .id)))))) ⟩ +-- lower ((((Prof*-o→Functor C D (LiftF ∘Fb R )) ⟅ y ⟆) +-- ⟪ G ⟪ ϕ ⟫ ⟫) ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ y ⟆)) +-- (lift (D .id)))) +-- -- since εy is defined in terms of R(Gy, y), we +-- -- first use naturality +-- -- to consider the relevant component of the εy ⋆ +-- -- map, namely the component at Gx +-- ≡⟨ (λ i → lower (((η⁻¹ .trans .N-ob y +-- .N-hom (G ⟪ ϕ ⟫)) (~ i)) (lift (D .id)) ) ) ⟩ +-- -- next, we use some recombining of G ϕ to see +-- -- it as an application +-- -- of a different Hom Functor applied to id at +-- -- Gx instead of Gy: +-- lower ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ x ⟆)) +-- (((Bifunctor→Functor (LiftF ∘Fb (HomBif D))) +-- ⟪ G ⟪ ϕ ⟫ , G ⟪ C .id ⟫ ⟫) (lift (D .id)))) +-- ≡⟨ (λ i → lower ((η⁻¹ .trans +-- .N-ob y .N-ob (G ⟅ x ⟆)) +-- (lift (((Bifunctor→Functor (HomBif D)) +-- ⟪ G ⟪ ϕ ⟫ , G .F-id i ⟫) (D .id)))) +-- )⟩ +-- lower ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ x ⟆)) +-- (lift (((Bifunctor→Functor (HomBif D)) ⟪ G ⟪ ϕ ⟫ , +-- D .id ⟫) (D .id)))) +-- ≡⟨ (λ i → lower ((η⁻¹ .trans .N-ob y .N-ob +-- (G ⟅ x ⟆)) (lift (((HomBif D) .Bif-idR (i) ∘f +-- (HomBif D) ⟪ G ⟪ ϕ ⟫ ⟫l ) (D .id))))) ⟩ +-- lower ((η⁻¹ .trans .N-ob y .N-ob (G ⟅ x ⟆)) +-- (lift (G ⟪ ϕ ⟫ ⋆⟨ D ⟩ D .id))) +-- ≡⟨ (λ i → lower ((η⁻¹ .trans .N-ob y .N-ob +-- (G ⟅ x ⟆)) (lift (D .⋆IdL (D .⋆IdR (G ⟪ ϕ ⟫) +-- (i)) (~ i))))) ⟩ +-- lower (((η⁻¹ .trans .N-ob y) .N-ob (G ⟅ x ⟆)) +-- (lift ((D .id) ⋆⟨ D ⟩ G ⟪ ϕ ⟫))) +-- ≡⟨ (λ i → lower ( +-- ((η⁻¹ .trans .N-ob y) .N-ob (G ⟅ x ⟆)) +-- (lift (((HomBif D) ⟪ G ⟪ ϕ ⟫ ⟫r ∘f +-- ((HomBif D) .Bif-idL (~ i))) (D .id))) +-- )) ⟩ +-- lower ( +-- ((η⁻¹ .trans .N-ob y) .N-ob (G ⟅ x ⟆)) +-- (lift (((Bifunctor→Functor (HomBif D)) +-- ⟪ D .id , G ⟪ ϕ ⟫ ⟫) (D .id))) +-- ) +-- ≡⟨ refl ⟩ +-- lower ( +-- ((((Prof*-o→Functor C D (LiftF ∘Fb +-- (Functor→Prof*-o C D G))) ⟪ ϕ ⟫) +-- ⋆⟨ FUNCTOR (D ^op) (SET _) ⟩ +-- η⁻¹ .trans .N-ob y) .N-ob (G ⟅ x ⟆)) +-- (lift (D .id)) +-- ) +-- -- now, since we are operating of the section of Gx +-- -- as described above, we +-- -- can use the above argument to port over to εx +-- ≡⟨ (λ i → lower ( +-- (((η⁻¹ .trans .N-hom ϕ) (i)) .N-ob (G ⟅ x ⟆)) +-- (lift (D .id)) +-- )) ⟩ +-- lower ( +-- ((η⁻¹ .trans .N-ob x +-- ⋆⟨ FUNCTOR (D ^op) (SET _) ⟩ +-- ((Prof*-o→Functor C D (LiftF ∘Fb R)) ⟪ ϕ ⟫) +-- ) .N-ob (G ⟅ x ⟆)) +-- (lift (D .id)) +-- ) +-- ≡⟨ (λ i → (R .Bif-assoc (D .id) ϕ (i)) εx) ⟩ +-- (R .Bif-homL (D .id) _) ((R .Bif-homR (G ⟅ x ⟆) ϕ) εx) +-- ≡⟨ ( λ i → (R .Bif-idL i) +-- ((R .Bif-homR (G ⟅ x ⟆) ϕ) εx))⟩ +-- ((R⟅dx,-⟆ ⟪ ϕ ⟫) εx) ∎ +-- ) +-- )⟩ +-- G ⟪ ϕ ⟫ ∎) +-- ) +-- in ΣPathP ( +-- G'≡G , +-- (makeNatIsoPathP +-- refl +-- (cong′ (λ X → Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb +-- Functor→Prof*-o C D X)) G'≡G) +-- (funExt (λ (c : C .ob) → +-- (makeNatTransPathP +-- refl +-- (cong′ (λ X → (Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb +-- Functor→Prof*-o C D X)) .F-ob c) G'≡G) +-- (funExt (λ (d : D .ob) → +-- (funExt λ _ → refl) +-- )) +-- ) +-- )) +-- ) +-- ) - ParamUnivElt≅ParamUniversalElement : Iso (ParamUnivElt C D R) - (ParamUniversalElement C D R) - ParamUnivElt≅ParamUniversalElement = - iso - (ParamUnivElt→ParamUniversalElement C D R) - (ParamUniversalElement→ParamUnivElt C D R) - (λ U → funExt λ c → Σ≡Prop - (isPropIsTerminal (∫ᴾ_ {C = D} (pAppR R c))) refl) - λ U → refl +-- ParamUnivElt≅ParamUniversalElement : Iso (ParamUnivElt C D R) +-- (ParamUniversalElement C D R) +-- ParamUnivElt≅ParamUniversalElement = +-- iso +-- (ParamUnivElt→ParamUniversalElement C D R) +-- (ParamUniversalElement→ParamUnivElt C D R) +-- (λ U → funExt λ c → Σ≡Prop +-- (isPropIsTerminal (∫ᴾ_ {C = D} (pAppR R c))) refl) +-- λ U → refl - ProfRepresentation≅ParamUnivElt : Iso (ProfRepresentation C D R) - (ParamUnivElt C D R) - ProfRepresentation≅ParamUnivElt = compIso - ProfRepresentation≅PshFunctorRepresentation - PshFunctorRepresentation≅ParamUnivElt +-- ProfRepresentation≅ParamUnivElt : Iso (ProfRepresentation C D R) +-- (ParamUnivElt C D R) +-- ProfRepresentation≅ParamUnivElt = compIso +-- ProfRepresentation≅PshFunctorRepresentation +-- PshFunctorRepresentation≅ParamUnivElt - ProfRepresentation≅ParamUniversalElement : Iso (ProfRepresentation C D R) - (ParamUniversalElement C D R) - ProfRepresentation≅ParamUniversalElement = compIso - ProfRepresentation≅ParamUnivElt - ParamUnivElt≅ParamUniversalElement +-- ProfRepresentation≅ParamUniversalElement : Iso (ProfRepresentation C D R) +-- (ParamUniversalElement C D R) +-- ProfRepresentation≅ParamUniversalElement = compIso +-- ProfRepresentation≅ParamUnivElt +-- ParamUnivElt≅ParamUniversalElement - PshFunctorRepresentation≅ParamUniversalElement : Iso - (PshFunctorRepresentation C D R) (ParamUniversalElement C D R) - PshFunctorRepresentation≅ParamUniversalElement = - compIso PshFunctorRepresentation≅ParamUnivElt - ParamUnivElt≅ParamUniversalElement +-- PshFunctorRepresentation≅ParamUniversalElement : Iso +-- (PshFunctorRepresentation C D R) (ParamUniversalElement C D R) +-- PshFunctorRepresentation≅ParamUniversalElement = +-- compIso PshFunctorRepresentation≅ParamUnivElt +-- ParamUnivElt≅ParamUniversalElement diff --git a/Cubical/Categories/Profunctor/General.agda b/Cubical/Categories/Profunctor/General.agda index 5fe39ddf..50508319 100644 --- a/Cubical/Categories/Profunctor/General.agda +++ b/Cubical/Categories/Profunctor/General.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} +{-# OPTIONS --safe --lossy-unification #-} module Cubical.Categories.Profunctor.General where open import Cubical.Reflection.RecordEquiv @@ -6,13 +6,14 @@ open import Cubical.Reflection.RecordEquiv open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv open import Cubical.Foundations.Structure open import Cubical.Foundations.Univalence open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Functor -open import Cubical.Categories.Bifunctor.Base +open import Cubical.Categories.Bifunctor.Redundant open import Cubical.Categories.Instances.Functors open import Cubical.Categories.NaturalTransformation open import Cubical.Categories.NaturalTransformation.More @@ -36,8 +37,7 @@ private open Category open Functor -open UnivElt -open isUniversal +open UniversalElement open Bifunctor -- Convenient notation for function composition in the same order as @@ -56,30 +56,13 @@ C o-[ ℓS ]-* D = Bifunctor (C ^op) D (SET ℓS) _*-[_]-o_ : (C : Category ℓC ℓC') → ∀ ℓS → (D : Category ℓD ℓD') → Type _ C *-[ ℓS ]-o D = D o-[ ℓS ]-* C -module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} {ℓS : Level} where - -- Product of a presheaf with a profunctor - -- This could be done by turning the presheaf into a profunctor - -- first but at the cost of extra ids. - _o×_ : (P : 𝓟o C ℓS) → (R : C o-[ ℓS ]-* D) → C o-[ ℓS ]-* D - (P o× R) .Bif-ob c d = - ⟨ P ⟅ c ⟆ ⟩ × ⟨ R ⟅ c , d ⟆b ⟩ , isSet× ((P ⟅ c ⟆) .snd) - ((R ⟅ c , d ⟆b) .snd) -- should be a combinator somewhere - (P o× R) .Bif-homL f d (p , r) = (P ⟪ f ⟫) p , (R ⟪ f ⟫l) r - (P o× R) .Bif-homR c g (p , r) = p , ((R ⟪ g ⟫r) r) - (P o× R) .Bif-idL = funExt λ (p , r) → λ i → (P .F-id i p , R .Bif-idL i r) - (P o× R) .Bif-idR = funExt λ (p , r) → λ i → (p , R .Bif-idR i r) - (P o× R) .Bif-seqL f f' = - funExt (λ (p , r) i → (P .F-seq f f' i p , R .Bif-seqL f f' i r)) - (P o× R) .Bif-seqR g g' = funExt (λ (p , r) i → (p , R .Bif-seqR g g' i r)) - (P o× R) .Bif-assoc f g = - funExt λ (p , r) i → ((P ⟪ f ⟫) p) , (R .Bif-assoc f g i r) - module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (R : C o-[ ℓR ]-* D) (S : C o-[ ℓS ]-* D) where - ℓmaxCDSR : Level - ℓmaxCDSR = (ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD (ℓ-max ℓD' (ℓ-max ℓS ℓR))))) + private + ℓmaxCDSR : Level + ℓmaxCDSR = (ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD (ℓ-max ℓD' (ℓ-max ℓS ℓR))))) -- A definition of profunctor homomorphism that avoids Lifts record ProfHomo : Type ℓmaxCDSR where @@ -153,6 +136,28 @@ module _ {C : Category ℓC ℓC'} ProfIso = Σ[ ϕ ∈ ProfHomo ] ∀ c d → isIso (ϕ .PH-ob {c}{d}) open ProfHomo +module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} {ℓS : Level} where + -- Product of a presheaf with a profunctor + -- This could be done by turning the presheaf into a profunctor + -- first but at the cost of extra ids. + _o×_ : (P : 𝓟o C ℓS) → (R : C o-[ ℓS ]-* D) → C o-[ ℓS ]-* D + (P o× R) = mkBifunctorParAx F where + open BifunctorParAx + F : BifunctorParAx (C ^op) D (SET ℓS) + F .Bif-ob c d = (⟨ P ⟅ c ⟆ ⟩ × ⟨ R ⟅ c , d ⟆b ⟩) + , (isSet× ((P ⟅ c ⟆) .snd) ((R ⟅ c , d ⟆b) .snd)) + F .Bif-homL f _ (p , r) = (P ⟪ f ⟫) p , (R ⟪ f ⟫l) r + F .Bif-homR _ g (p , r) = p , ((R ⟪ g ⟫r) r) + F .Bif-hom× f g (p , r) = ((P ⟪ f ⟫) p) , ((R ⟪ f , g ⟫×) r) + F .Bif-×-id = funExt (λ (p , r) → ΣPathP ((funExt⁻ (P .F-id) _) + , funExt⁻ (R .Bif-×-id) _)) + F .Bif-×-seq f f' g g' = funExt (λ (p , r) → ΣPathP ( + ( funExt⁻ (P .F-seq f f') _) + , funExt⁻ (R .Bif-×-seq f f' g g') _)) + F .Bif-L×-agree f = funExt (λ (p , r) → ΣPathP (refl + , (funExt⁻ (R .Bif-L×-agree _) _))) + F .Bif-R×-agree g = funExt (λ (p , r) → ΣPathP ((sym (funExt⁻ (P .F-id) _)) + , funExt⁻ (R .Bif-R×-agree _) _)) Functor→Prof*-o : (C : Category ℓC ℓC') (D : Category ℓD ℓD') (F : Functor C D) → C *-[ ℓD' ]-o D @@ -162,435 +167,467 @@ Functor→Profo-* : (C : Category ℓC ℓC') (D : Category ℓD ℓD') (F : Functor C D) → C o-[ ℓD' ]-* D Functor→Profo-* C D F = HomBif D ∘Fl (F ^opF) -Prof*-o→Functor : (C : Category ℓC ℓC') - (D : Category ℓD ℓD') (R : C *-[ ℓS ]-o D) → - Functor C (FUNCTOR (D ^op) (SET ℓS)) -Prof*-o→Functor C D R = curryFl (D ^op) (SET _) ⟅ Bifunctor→Functor R ⟆ +-- Prof*-o→Functor : (C : Category ℓC ℓC') +-- (D : Category ℓD ℓD') (R : C *-[ ℓS ]-o D) → +-- Functor C (FUNCTOR (D ^op) (SET ℓS)) +-- Prof*-o→Functor C D R = curryFl (D ^op) (SET _) ⟅ Bifunctor→Functor R ⟆ -Profo-*→Functor : (C : Category ℓC ℓC') - (D : Category ℓD ℓD') (R : C o-[ ℓS ]-* D) → - Functor (C ^op) (FUNCTOR D (SET ℓS)) -Profo-*→Functor C D R = curryF D (SET _) ⟅ Bifunctor→Functor R ⟆ +-- Profo-*→Functor : (C : Category ℓC ℓC') +-- (D : Category ℓD ℓD') (R : C o-[ ℓS ]-* D) → +-- Functor (C ^op) (FUNCTOR D (SET ℓS)) +-- Profo-*→Functor C D R = curryF D (SET _) ⟅ Bifunctor→Functor R ⟆ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') (R : C *-[ ℓS ]-o D) where open NatTrans open NatIso open isIsoC - - ProfRepresents : Functor C D → Type _ - ProfRepresents G = ProfIso {C = D}{D = C} R (Functor→Prof*-o C D G) - - ProfRepresentation : Type _ - ProfRepresentation = Σ[ G ∈ Functor C D ] ProfRepresents G - - PshFunctorRepresentation : Type _ - PshFunctorRepresentation = - Σ[ G ∈ Functor C D ] - NatIso (Prof*-o→Functor C D ((LiftF {ℓS}{ℓD'}) ∘Fb R )) - (Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb (Functor→Prof*-o C D G))) - - RepresentableAt : (c : C .ob) → Type _ - RepresentableAt c = UnivElt D (pAppR R c) - - ParamUnivElt : Type _ - ParamUnivElt = (c : C .ob) → RepresentableAt c - - ParamUniversalElement : Type _ - ParamUniversalElement = (c : C .ob) → UniversalElement D (pAppR R c) - - {- - ProfRepresentation, PshFunctorRepresentation, ParamUnivElt, - and ParamUniversalElement - each give a different criterion for a profunctor R to be representable. - - These are all equivalent, and the equivalence is witnessed by - the following functions. - Below we simply provide the functions, and in Profunctor.Equivalence - we prove - that they do indeed provide type isomorphisms. - -} - - -- ProfRepresentation → PshFunctorRepresentation - ProfRepresentation→PshFunctorRepresentation : ProfRepresentation → - PshFunctorRepresentation - ProfRepresentation→PshFunctorRepresentation (G , η) = - G , - record { - trans = the-trans ; - nIso = λ c → - FUNCTORIso - (D ^op) - (SET (ℓ-max ℓD' ℓS)) - (the-trans .N-ob c) - λ d → - isiso - (λ x → lift ((η .snd d c .fst) (lower x))) - (λ i x → lift ((η .snd d c .snd .fst) (lower x) i)) - (λ i x → lift ((η .snd d c .snd .snd) (lower x) i)) - } - where - the-trans : NatTrans (Prof*-o→Functor C D (bifCompF LiftF R)) - (Prof*-o→Functor C D (bifCompF LiftF (Functor→Prof*-o C D G))) - the-trans .N-ob c = - natTrans - (λ d x → lift (η .fst .PH-ob (lower x))) - (λ f → funExt (λ x → - (Prof*-o→Functor C D (bifCompF LiftF R) .F-ob c .F-hom f - ⋆f - (λ x₂ → lift (η .fst .PH-ob (lower x₂)))) x - ≡⟨ (λ i → lift (η .fst .PH-ob (((R ⟪ f ⟫l) ⋆f - R .Bif-idR i) (lower x)))) ⟩ - lift (PH-ob (η .fst) ((R ⟪ f ⟫l) (lower x))) - ≡⟨ (λ i → lift (η .fst .PH-natL f (lower x) i)) ⟩ - lift ((Functor→Prof*-o C D G ⟪ f ⟫l) (PH-ob (η .fst) (lower x))) - ≡⟨ (λ i → lift (((Functor→Prof*-o C D G) ⟪ f ⟫l ⋆f - Functor→Prof*-o C D G .Bif-idR (~ i)) - (η .fst .PH-ob (lower x)))) ⟩ - ((λ x₂ → lift (η .fst .PH-ob (lower x₂))) - ⋆f - Prof*-o→Functor C D (bifCompF LiftF (Functor→Prof*-o C D G)) - .F-ob c .F-hom f) x ∎ - )) - the-trans .N-hom f = - makeNatTransPath - (funExt (λ d → funExt λ x → - lift (η .fst .PH-ob ((Bif-homL R (id D) _ ⋆f - (R ⟪ f ⟫r)) (lower x))) - ≡⟨ (λ i → lift (η .fst .PH-ob ((R .Bif-idL i ⋆f - (R ⟪ f ⟫r)) (lower x)))) ⟩ - lift (PH-ob (η .fst) ((R ⟪ f ⟫r) (lower x))) - ≡⟨ (λ i → lift (η .fst .PH-natR (lower x) f i)) ⟩ - lift ((Functor→Prof*-o C D G ⟪ f ⟫r) (PH-ob (η .fst) (lower x))) - ≡⟨ ((λ i → lift ((Functor→Prof*-o C D G .Bif-idL (~ i) ⋆f - (Functor→Prof*-o C D G ⟪ f ⟫r )) - (η .fst .PH-ob (lower x))))) ⟩ - lift - ((Bif-homL (Functor→Prof*-o C D G) (id D) _ ⋆f - (Functor→Prof*-o C D G ⟪ f ⟫r)) - (η .fst .PH-ob (lower x))) ∎)) - - -- PshFunctor Representation → ProfRepresentation - PshFunctorRepresentation→ProfRepresentation : PshFunctorRepresentation → - ProfRepresentation - PshFunctorRepresentation→ProfRepresentation (G , η) = - G , - (record { - PH-ob = λ {d}{c} r → lower ((η .trans .N-ob c .N-ob d) (lift r)) ; - PH-natL = λ {d}{d'}{c} f r → - lower (((η .trans .N-ob c .N-ob d) ∘f - ((bifCompF LiftF R) .Bif-homL f c)) (lift r)) - ≡⟨ ((λ i → lower (((η .trans .N-ob c .N-ob d) ∘f - ( (bifCompF LiftF R) .Bif-homL f c ⋆f - (bifCompF LiftF R) .Bif-idR (~ i))) (lift r)))) ⟩ - lower (((η .trans .N-ob c .N-ob d) ∘f - (((bifCompF LiftF R) .Bif-homL f c) ⋆f - (bifCompF LiftF R) .Bif-homR d (C .id))) (lift r)) - ≡⟨ ((λ i → lower ((η .trans .N-ob c .N-hom f i) (lift r)))) ⟩ - lower ((N-ob (η .trans .N-ob c) d' ⋆f - Prof*-o→Functor C D (bifCompF LiftF (Functor→Prof*-o C D G)) - .F-ob c .F-hom f) (lift r)) - ≡⟨ ((λ i → ((Functor→Prof*-o C D G ⟪ f ⟫l) ⋆f - (Functor→Prof*-o C D G) .Bif-idR i) - (lower (η .trans .N-ob c .N-ob d' (lift r))))) ⟩ - (Functor→Prof*-o C D G ⟪ f ⟫l) - (lower (η .trans .N-ob c .N-ob d' (lift r))) ∎ - ; - PH-natR = λ {c}{d}{d'} r g → - lower (η .trans .N-ob d' .N-ob c (lift ((R ⟪ g ⟫r) r))) - ≡⟨ (λ i → lower (η .trans .N-ob d' .N-ob c - (lift ((R .Bif-idL (~ i) ⋆f R ⟪ g ⟫r) r)))) ⟩ - lower - ((Prof*-o→Functor C D (bifCompF LiftF R) .F-hom g .N-ob c ⋆f - N-ob (η .trans) d' .N-ob c) (lift r)) - ≡⟨ (λ i → lower ((η .trans .N-hom g i .N-ob c) (lift r))) ⟩ - lower ((N-ob (η .trans) d .N-ob c ⋆f - Prof*-o→Functor C D (bifCompF LiftF (Functor→Prof*-o C D G)) - .F-hom g .N-ob c) (lift r)) - ≡⟨ ((λ i → (Functor→Prof*-o C D G .Bif-idL i ⋆f - (Functor→Prof*-o C D G ⟪ g ⟫r)) - (lower (η .trans .N-ob d .N-ob c (lift r))))) ⟩ - (Functor→Prof*-o C D G ⟪ g ⟫r) - (lower (η .trans .N-ob d .N-ob c (lift r))) ∎ - }) , - λ d c → - (λ x → lower (η .nIso c .inv .N-ob d (lift x))) , - (λ x i → lower ((η .nIso c .sec i .N-ob d) (lift x))) , - (λ x i → lower((η .nIso c .ret i .N-ob d) (lift x))) - - open NatIso - open NatTrans - open isIsoC - - -- PshFunctorRepresentation → ParamUnivElt - PshFunctorRepresentation→ParamUnivElt : PshFunctorRepresentation → - ParamUnivElt - PshFunctorRepresentation→ParamUnivElt (G , η) = (λ c → - let R⟅-,c⟆ = (pAppR R c) in - let η⁻¹ = symNatIso η in - record { - vertex = (G ⟅ c ⟆) ; - element = lower ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id))) ; - universal = record { - coinduction = λ {d} ϕ → lower ((η .trans .N-ob c .N-ob d) (lift ϕ)); - commutes = (λ {d} ϕ → - let coindϕ = (lower ((η .trans .N-ob c .N-ob d) (lift ϕ))) in - lower (((LiftF ∘F R⟅-,c⟆) ⟪ coindϕ ⟫) - ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id)))) - ≡⟨ (λ i → lower (((LiftF ∘Fb R ) .Bif-idR (~ i)) - (((LiftF ∘Fb R ) .Bif-homL coindϕ c) - ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id)))))) ⟩ - lower ((((Prof*-o→Functor C D ((LiftF {ℓS}{ℓD'}) ∘Fb R )) ⟅ c ⟆) - ⟪ coindϕ ⟫) ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id)))) - ≡⟨ (λ i → lower ((((η⁻¹ .trans .N-ob c .N-hom coindϕ) (~ i)) - (lift (D .id))))) ⟩ - lower ((η⁻¹ .trans .N-ob c .N-ob d) - (((Bifunctor→Functor ((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D))) - ⟪ coindϕ , G ⟪ C .id ⟫ ⟫) (lift (D .id)))) - ≡⟨ ( λ i → lower ((η⁻¹ .trans .N-ob c .N-ob d) - (((Bifunctor→Functor ((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D))) - ⟪ coindϕ , G .F-id (i) ⟫) (lift (D .id))))) ⟩ - lower ((η⁻¹ .trans .N-ob c .N-ob d) - (((Bifunctor→Functor ((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D))) - ⟪ coindϕ , D .id ⟫) (lift (D .id)))) - ≡⟨ (λ i → - lower ((η⁻¹ .trans .N-ob c .N-ob d) - ((((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D)) .Bif-idR (i)) - ((((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D)) .Bif-homL coindϕ - (G ⟅ c ⟆)) (lift (D .id)))) - ) - ) ⟩ - lower ((η⁻¹ .trans .N-ob c .N-ob d) (lift (coindϕ ⋆⟨ D ⟩ (D .id)))) - ≡⟨ (λ i → lower ((η⁻¹ .trans .N-ob c .N-ob d) - (lift (D .⋆IdR coindϕ (i))))) ⟩ - lower ((η⁻¹ .trans .N-ob c .N-ob d) (lift (coindϕ))) - ≡⟨ (λ i → lower ((((η .nIso c .ret) (i)) .N-ob d) (lift ϕ))) ⟩ - ϕ ∎) ; - is-uniq = - λ {d} ϕ f ε⋆f≡ϕ → - let coindϕ = (lower ((η .trans .N-ob c .N-ob d) (lift ϕ))) in - f - ≡⟨ sym (D .⋆IdR f) ⟩ - (f ⋆⟨ D ⟩ D .id) - ≡⟨ (λ i → (((HomBif D) .Bif-idR (~ i)) - (((HomBif D) .Bif-homL f (G ⟅ c ⟆)) (D .id)))) ⟩ - (((Bifunctor→Functor (HomBif D)) ⟪ f , D .id ⟫) (D .id)) - ≡⟨ (λ i → (((Bifunctor→Functor (HomBif D)) - ⟪ f , G .F-id (~ i) ⟫) (D .id))) ⟩ - (((Bifunctor→Functor (HomBif D)) ⟪ f , G ⟪ C .id ⟫ ⟫) (D .id)) - ≡⟨ (λ i → lower(((η .nIso c .sec) (~ i) .N-ob d) - (lift (((Bifunctor→Functor (HomBif D)) - ⟪ f , G ⟪ C .id ⟫ ⟫) (D .id))))) ⟩ - lower ((η .trans .N-ob c .N-ob d) - ((η⁻¹ .trans .N-ob c .N-ob d) - (lift (((Bifunctor→Functor (HomBif D)) - ⟪ f , G ⟪ C .id ⟫ ⟫) (D .id))))) - ≡⟨ (λ i → lower ((η .trans .N-ob c .N-ob d) - (((η⁻¹ .trans .N-ob c .N-hom f) (i)) (lift (D .id))))) ⟩ - lower ((η .trans .N-ob c .N-ob d) - ((((Prof*-o→Functor C D ((LiftF {ℓS}{ℓD'}) ∘Fb R )) ⟅ c ⟆) ⟪ f ⟫) - ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id))))) - ≡⟨ ( λ i → lower ((η .trans .N-ob c .N-ob d) - (((LiftF ∘Fb R ) .Bif-idR (i)) (((LiftF ∘Fb R ) .Bif-homL f c) - ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id))))))) ⟩ - lower ((η .trans .N-ob c .N-ob d) (lift ((R⟅-,c⟆ ⟪ f ⟫) - (lower ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id))))))) - ≡⟨ (λ i → (lower ((η .trans .N-ob c .N-ob d) - (lift (ε⋆f≡ϕ i))))) ⟩ - coindϕ ∎ - } - } - ) - - ParamUnivElt→Functor : ParamUnivElt → Functor C D - ParamUnivElt→Functor ues .F-ob c = ues c .vertex - ParamUnivElt→Functor ues .F-hom {x = c}{y = c'} f = - ues c' .universal .coinduction ((R ⟪ f ⟫r) (ues c .element)) - ParamUnivElt→Functor ues .F-id {x = c} = - cong (ues c .universal .coinduction) (λ i → R .Bif-idR i (ues c .element)) - ∙ sym (coinduction-elt (ues c .universal)) - ParamUnivElt→Functor ues .F-seq {x = c}{y = c'}{z = c''} f g = - -- Both sides are ≡ to R .Bif-homR (ues c .vertex) g - -- (R .Bif-homR (ues c .vertex) f (ues c .element)) - cong (ues c'' .universal .coinduction) - ((λ i → R .Bif-seqR f g i (ues c .element))) - ∙ cong (coinduction (ues c'' .universal)) - ( cong (R .Bif-homR (ues c .vertex) g) - (sym (ues c' .universal .commutes _)) - ∙ (λ i → R .Bif-assoc (ues c' .universal .coinduction ((R ⟪ f ⟫r) - (ues c .element))) g i (ues c' .element))) - ∙ sym (coinduction-natural (ues c'' .universal) _ _) - - -- ParamUnivElt → PshFunctorRepresentation - ParamUnivElt→PshFunctorRepresentation : ParamUnivElt → - PshFunctorRepresentation - ParamUnivElt→PshFunctorRepresentation ues = - (representing-functor , representing-nat-iso) where - representing-functor : Functor C D - representing-functor = ParamUnivElt→Functor ues - - rep-nat-iso-trans : (c : C .ob) → - NatTrans (Prof*-o→Functor C D (LiftF {ℓS}{ℓD'} ∘Fb R) .F-ob c) - (Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb - (Functor→Prof*-o C D representing-functor)) .F-ob c) - rep-nat-iso-trans c .N-ob d = - let R⟅-,c⟆ = (pAppR R c) in - (λ f → lift {ℓD'}{ℓS} ((ues c) .universal .coinduction {b = d} - (lower {ℓS}{ℓD'} f))) - rep-nat-iso-trans c .N-hom {d}{d'} ϕ = - let R⟅-,c⟆ = (pAppR R c) in - let εc = ues c .element in - let coind = (ues c) .universal .coinduction in - funExt λ x → - lift (coind (((Prof*-o→Functor C D R .F-ob c) ⟪ ϕ ⟫) (lower x))) - ≡⟨ ( λ i → lift (coind ((R .Bif-idR (i)) ((R .Bif-homL ϕ c) - (lower x))))) ⟩ - lift (coind (D [ (lower x) ∘ᴾ⟨ R⟅-,c⟆ ⟩ ϕ ] )) - ≡⟨ (λ i → lift ((coinduction-natural ((ues c) .universal) - (lower x) ϕ) (~ i))) ⟩ - lift ((coind (lower x)) ∘⟨ D ⟩ ϕ ) - ≡⟨ (λ i → lift (((HomBif D) .Bif-idR (~ i)) - (((HomBif D) .Bif-homL ϕ _) (coind (lower x)))) ) ⟩ - lift (((Bifunctor→Functor (HomBif D)) ⟪ ϕ , D .id ⟫ ) (coind (lower x))) - ≡⟨ (λ i → lift (((Bifunctor→Functor (HomBif D)) - ⟪ ϕ , representing-functor .F-id (~ i) ⟫ ) (coind (lower x)))) ⟩ - lift (((Bifunctor→Functor (HomBif D)) - ⟪ ϕ , representing-functor ⟪ C . id ⟫ ⟫ ) (coind (lower x))) ∎ - - representing-nat-iso : NatIso - (Prof*-o→Functor C D (LiftF {ℓS}{ℓD'} ∘Fb R)) - (Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb - (Functor→Prof*-o C D representing-functor))) - representing-nat-iso .trans .N-ob c = rep-nat-iso-trans c - representing-nat-iso .trans .N-hom {x}{y} ψ = - let R⟅-,x⟆ = (pAppR R x) in - let R⟅-,y⟆ = (pAppR R y) in - let εy = ues y .element in - let εx = ues x .element in - let coindx = ues x .universal .coinduction in - let coindy = ues y .universal .coinduction in - makeNatTransPath (funExt (λ d → funExt (λ α → - lift (coindy (((Bifunctor→Functor R) ⟪ D .id , ψ ⟫) (lower α))) - ≡⟨ (λ i → lift (coindy - (R .Bif-homR _ ψ ((R .Bif-idL (i)) (lower α))))) ⟩ - lift (coindy (R .Bif-homR _ ψ (lower α))) - ≡⟨ ( λ i → lift (ues y .universal .is-uniq - (R .Bif-homR _ ψ (lower α)) - ((coindx (lower α)) ⋆⟨ D ⟩ (representing-functor ⟪ ψ ⟫)) - ( - ( - D [ εy ∘ᴾ⟨ R⟅-,y⟆ ⟩ (coindy ((R .Bif-homR _ ψ) εx) ∘⟨ D ⟩ - (coindx (lower α))) ] - ≡⟨ (λ i → D [ - εy ∘ᴾ⟨ R⟅-,y⟆ ⟩ ((coinduction-natural (ues y .universal) - ((R .Bif-homR _ ψ) εx) (coindx (lower α))) i)] ) ⟩ - D [ εy ∘ᴾ⟨ R⟅-,y⟆ ⟩ - coindy ( D [ ((R .Bif-homR _ ψ) εx) ∘ᴾ⟨ R⟅-,y⟆ ⟩ - (coindx (lower α)) ]) ] - ≡⟨ ues y .universal .commutes - (D [ ((R .Bif-homR _ ψ) εx) ∘ᴾ⟨ R⟅-,y⟆ ⟩ - (coindx (lower α)) ]) ⟩ - D [ ((R .Bif-homR _ ψ) εx) ∘ᴾ⟨ R⟅-,y⟆ ⟩ (coindx (lower α)) ] - ≡⟨ (λ i → ((R .Bif-assoc (coindx (lower α)) ψ) (~ i)) εx) ⟩ - (R .Bif-homR _ ψ) (D [ εx ∘ᴾ⟨ R⟅-,x⟆ ⟩ (coindx (lower α)) ]) - ≡⟨ (λ i → (R .Bif-homR _ ψ) - (ues x .universal .commutes (lower α) (i))) ⟩ - (R .Bif-homR _ ψ (lower α)) ∎ - ) - ) - (~ i))) ⟩ - lift ((coindx (lower α)) ⋆⟨ D ⟩ (representing-functor ⟪ ψ ⟫)) - ≡⟨ (λ i → lift ((HomBif D) .Bif-homR _ (representing-functor ⟪ ψ ⟫) - (((HomBif D) .Bif-idL (~ i)) (coindx (lower α))))) ⟩ - lift (((Bifunctor→Functor (HomBif D)) ⟪ D .id , - representing-functor ⟪ ψ ⟫ ⟫) (coindx (lower α))) ∎ - - ))) - representing-nat-iso .nIso c .inv .N-ob d = - let εc = ues c .element in - let R⟅-,c⟆ = (pAppR R c) in - λ f → lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (lower f) ]) - representing-nat-iso .nIso c .inv .N-hom {d}{d'} ϕ = - let εc = ues c .element in - let R⟅-,c⟆ =(pAppR R c) in - funExt λ x → - lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ ((Bifunctor→Functor (HomBif D)) - ⟪ ϕ , representing-functor ⟪ C .id ⟫ ⟫) (lower x) ]) - ≡⟨ (λ i → lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ ((Bifunctor→Functor (HomBif D)) - ⟪ ϕ , representing-functor .F-id i ⟫) (lower x) ])) ⟩ - lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ ((Bifunctor→Functor (HomBif D)) - ⟪ ϕ , D .id ⟫ ) (lower x) ]) - ≡⟨ (λ i → lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ ((HomBif D) .Bif-idR (i) - (((HomBif D) .Bif-homL ϕ _) (lower x))) ])) ⟩ - lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (ϕ ⋆⟨ D ⟩ (lower x)) ]) - ≡⟨ (λ i → lift (((R⟅-,c⟆ .F-seq (lower x) ϕ) i) εc)) ⟩ - lift ((R .Bif-homL ϕ _) (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (lower x) ])) - ≡⟨ (λ i → lift ((R .Bif-idR (~ i)) ((R .Bif-homL ϕ _) - (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (lower x) ])))) ⟩ - lift (((Bifunctor→Functor R) ⟪ ϕ , C .id ⟫) - (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (lower x) ])) ∎ - - representing-nat-iso .nIso c .sec = - let R⟅-,c⟆ = (pAppR R c) in - makeNatTransPath (funExt λ d → funExt λ x → (λ i → - lift ((η-expansion ((ues c) .universal) (lower x)) (~ i))) ) - representing-nat-iso .nIso c .ret = - let R⟅-,c⟆ = (pAppR R c) in - makeNatTransPath (funExt λ d → funExt λ x → (λ i → - lift (((ues c) .universal .commutes (lower x)) i))) - - -- ParamUniversalElement → ParamUnivElt - ParamUniversalElement→ParamUnivElt : ParamUniversalElement → ParamUnivElt - ParamUniversalElement→ParamUnivElt U c = - UniversalElement→UnivElt D (pAppR R c) (U c) - - -- ParamUnivElt → ParamUniversalElement - ParamUnivElt→ParamUniversalElement : ParamUnivElt → ParamUniversalElement - ParamUnivElt→ParamUniversalElement U c = - UnivElt→UniversalElement D (pAppR R c) (U c) - - {- - We have now given maps - ProfRepresentation ⇔ PshFunctorRepresentation - PshFunctorRepresentation ⇔ ParamUnivElt - ParamUnivElt ⇔ ParamUniversalElement - - For convenience, - below we also stitch these together to give all pairwise maps. - -} - - -- ProfRepresentation → ParamUnivElt - ProfRepresentation→ParamUnivElt : ProfRepresentation → ParamUnivElt - ProfRepresentation→ParamUnivElt R = - PshFunctorRepresentation→ParamUnivElt - (ProfRepresentation→PshFunctorRepresentation R) - - -- ProfRepresentation → ParamUniversalElement - ProfRepresentation→ParamUniversalElement : ProfRepresentation → - ParamUniversalElement - ProfRepresentation→ParamUniversalElement R = - ParamUnivElt→ParamUniversalElement (ProfRepresentation→ParamUnivElt R) - - -- PshFunctorRepresentation → ParamUniversalElement - PshFunctorRepresentation→ParamUniversalElement : PshFunctorRepresentation → - ParamUniversalElement - PshFunctorRepresentation→ParamUniversalElement R = - ParamUnivElt→ParamUniversalElement (PshFunctorRepresentation→ParamUnivElt R) - - -- ParamUnivElt → ProfRepresentation - ParamUnivElt→ProfRepresentation : ParamUnivElt → ProfRepresentation - ParamUnivElt→ProfRepresentation U = - PshFunctorRepresentation→ProfRepresentation - (ParamUnivElt→PshFunctorRepresentation U) - - -- ParamUniversalElement → ProfRepresentation - ParamUniversalElement→ProfRepresentation : ParamUniversalElement → - ProfRepresentation - ParamUniversalElement→ProfRepresentation U = - ParamUnivElt→ProfRepresentation (ParamUniversalElement→ParamUnivElt U) - - -- ParamUniversalElement → PshFunctorRepresentation - ParamUniversalElement→PshFunctorRepresentation : ParamUniversalElement → - PshFunctorRepresentation - ParamUniversalElement→PshFunctorRepresentation U = - ParamUnivElt→PshFunctorRepresentation (ParamUniversalElement→ParamUnivElt U) + open isEquiv + + UniversalElementAt : C .ob → Type _ + UniversalElementAt c = UniversalElement D (appR R c) + + UniversalElements : Type _ + UniversalElements = ((∀ (c : C .ob) → UniversalElement D (appR R c))) + + FunctorComprehension : + ((∀ (c : C .ob) → UniversalElement D (appR R c))) + → Σ[ F ∈ Functor C D ] (∀ (c : C .ob) + → UniversalElementOn D (appR R c) (F ⟅ c ⟆)) + FunctorComprehension ues = F , + (λ c → UniversalElementToUniversalElementOn _ _ (ues c)) where + F : Functor C D + F .F-ob c = ues c .vertex + F .F-hom f = + ues _ .universal _ .equiv-proof ((R ⟪ f ⟫r) (ues _ .element)) + .fst .fst + F .F-id {x = c} = cong fst (ues c .universal (ues c .vertex) .equiv-proof + ((R ⟪ C .id ⟫r) (ues _ .element)) .snd (_ , + funExt⁻ (R .Bif-L-id) _ + ∙ sym (funExt⁻ (R .Bif-R-id) _))) + F .F-seq f g = cong fst ((ues _ .universal (ues _ .vertex) .equiv-proof + ((R ⟪ f ⋆⟨ C ⟩ g ⟫r) (ues _ .element))) .snd (_ , + funExt⁻ (R .Bif-L-seq _ _) _ + ∙ cong (R .Bif-homL _ _) (ues _ .universal _ .equiv-proof + ((R ⟪ g ⟫r) (ues _ .element)) .fst .snd) + ∙ funExt⁻ ( (Bif-RL-commute R _ _)) _ + ∙ cong (R .Bif-homR _ _) ((ues _ .universal _ .equiv-proof + ((R ⟪ f ⟫r) (ues _ .element)) .fst .snd)) + ∙ sym (funExt⁻ (R .Bif-R-seq _ _) _) )) + + -- ProfRepresents : Functor C D → Type _ + -- ProfRepresents G = ProfIso {C = D}{D = C} R (Functor→Prof*-o C D G) + + -- ProfRepresentation : Type _ + -- ProfRepresentation = Σ[ G ∈ Functor C D ] ProfRepresents G + + -- PshFunctorRepresentation : Type _ + -- PshFunctorRepresentation = + -- Σ[ G ∈ Functor C D ] + -- NatIso (Prof*-o→Functor C D ((LiftF {ℓS}{ℓD'}) ∘Fb R )) + -- (Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb (Functor→Prof*-o C D G))) + + -- RepresentableAt : (c : C .ob) → Type _ + -- RepresentableAt c = UniversalElement D (pAppR R c) + + -- ParamUnivElt : Type _ + -- ParamUnivElt = (c : C .ob) → RepresentableAt c + + -- ParamUniversalElement : Type _ + -- ParamUniversalElement = (c : C .ob) → UniversalElement D (pAppR R c) + + -- {- + -- ProfRepresentation, PshFunctorRepresentation, ParamUnivElt, + -- and ParamUniversalElement + -- each give a different criterion for a profunctor R to be representable. + + -- These are all equivalent, and the equivalence is witnessed by + -- the following functions. + -- Below we simply provide the functions, and in Profunctor.Equivalence + -- we prove + -- that they do indeed provide type isomorphisms. + -- -} + + -- -- ProfRepresentation → PshFunctorRepresentation + -- ProfRepresentation→PshFunctorRepresentation : ProfRepresentation → + -- PshFunctorRepresentation + -- ProfRepresentation→PshFunctorRepresentation (G , η) = + -- G , + -- record { + -- trans = the-trans ; + -- nIso = λ c → + -- FUNCTORIso + -- (D ^op) + -- (SET (ℓ-max ℓD' ℓS)) + -- (the-trans .N-ob c) + -- λ d → + -- isiso + -- (λ x → lift ((η .snd d c .fst) (lower x))) + -- (λ i x → lift ((η .snd d c .snd .fst) (lower x) i)) + -- (λ i x → lift ((η .snd d c .snd .snd) (lower x) i)) + -- } + -- where + -- the-trans : NatTrans (Prof*-o→Functor C D (bifCompF LiftF R)) + -- (Prof*-o→Functor C D (bifCompF LiftF (Functor→Prof*-o C D G))) + -- the-trans .N-ob c = + -- natTrans + -- (λ d x → lift (η .fst .PH-ob (lower x))) + -- (λ f → funExt (λ x → + -- (Prof*-o→Functor C D (bifCompF LiftF R) .F-ob c .F-hom f + -- ⋆f + -- (λ x₂ → lift (η .fst .PH-ob (lower x₂)))) x + -- ≡⟨ (λ i → lift (η .fst .PH-ob (((R ⟪ f ⟫l) ⋆f + -- R .Bif-idR i) (lower x)))) ⟩ + -- lift (PH-ob (η .fst) ((R ⟪ f ⟫l) (lower x))) + -- ≡⟨ (λ i → lift (η .fst .PH-natL f (lower x) i)) ⟩ + -- lift ((Functor→Prof*-o C D G ⟪ f ⟫l) (PH-ob (η .fst) (lower x))) + -- ≡⟨ (λ i → lift (((Functor→Prof*-o C D G) ⟪ f ⟫l ⋆f + -- Functor→Prof*-o C D G .Bif-idR (~ i)) + -- (η .fst .PH-ob (lower x)))) ⟩ + -- ((λ x₂ → lift (η .fst .PH-ob (lower x₂))) + -- ⋆f + -- Prof*-o→Functor C D (bifCompF LiftF (Functor→Prof*-o C D G)) + -- .F-ob c .F-hom f) x ∎ + -- )) + -- the-trans .N-hom f = + -- makeNatTransPath + -- (funExt (λ d → funExt λ x → + -- lift (η .fst .PH-ob ((Bif-homL R (id D) _ ⋆f + -- (R ⟪ f ⟫r)) (lower x))) + -- ≡⟨ (λ i → lift (η .fst .PH-ob ((R .Bif-idL i ⋆f + -- (R ⟪ f ⟫r)) (lower x)))) ⟩ + -- lift (PH-ob (η .fst) ((R ⟪ f ⟫r) (lower x))) + -- ≡⟨ (λ i → lift (η .fst .PH-natR (lower x) f i)) ⟩ + -- lift ((Functor→Prof*-o C D G ⟪ f ⟫r) (PH-ob (η .fst) (lower x))) + -- ≡⟨ ((λ i → lift ((Functor→Prof*-o C D G .Bif-idL (~ i) ⋆f + -- (Functor→Prof*-o C D G ⟪ f ⟫r )) + -- (η .fst .PH-ob (lower x))))) ⟩ + -- lift + -- ((Bif-homL (Functor→Prof*-o C D G) (id D) _ ⋆f + -- (Functor→Prof*-o C D G ⟪ f ⟫r)) + -- (η .fst .PH-ob (lower x))) ∎)) + + -- -- PshFunctor Representation → ProfRepresentation + -- PshFunctorRepresentation→ProfRepresentation : PshFunctorRepresentation → + -- ProfRepresentation + -- PshFunctorRepresentation→ProfRepresentation (G , η) = + -- G , + -- (record { + -- PH-ob = λ {d}{c} r → lower ((η .trans .N-ob c .N-ob d) (lift r)) ; + -- PH-natL = λ {d}{d'}{c} f r → + -- lower (((η .trans .N-ob c .N-ob d) ∘f + -- ((bifCompF LiftF R) .Bif-homL f c)) (lift r)) + -- ≡⟨ ((λ i → lower (((η .trans .N-ob c .N-ob d) ∘f + -- ( (bifCompF LiftF R) .Bif-homL f c ⋆f + -- (bifCompF LiftF R) .Bif-idR (~ i))) (lift r)))) ⟩ + -- lower (((η .trans .N-ob c .N-ob d) ∘f + -- (((bifCompF LiftF R) .Bif-homL f c) ⋆f + -- (bifCompF LiftF R) .Bif-homR d (C .id))) (lift r)) + -- ≡⟨ ((λ i → lower ((η .trans .N-ob c .N-hom f i) (lift r)))) ⟩ + -- lower ((N-ob (η .trans .N-ob c) d' ⋆f + -- Prof*-o→Functor C D (bifCompF LiftF (Functor→Prof*-o C D G)) + -- .F-ob c .F-hom f) (lift r)) + -- ≡⟨ ((λ i → ((Functor→Prof*-o C D G ⟪ f ⟫l) ⋆f + -- (Functor→Prof*-o C D G) .Bif-idR i) + -- (lower (η .trans .N-ob c .N-ob d' (lift r))))) ⟩ + -- (Functor→Prof*-o C D G ⟪ f ⟫l) + -- (lower (η .trans .N-ob c .N-ob d' (lift r))) ∎ + -- ; + -- PH-natR = λ {c}{d}{d'} r g → + -- lower (η .trans .N-ob d' .N-ob c (lift ((R ⟪ g ⟫r) r))) + -- ≡⟨ (λ i → lower (η .trans .N-ob d' .N-ob c + -- (lift ((R .Bif-idL (~ i) ⋆f R ⟪ g ⟫r) r)))) ⟩ + -- lower + -- ((Prof*-o→Functor C D (bifCompF LiftF R) .F-hom g .N-ob c ⋆f + -- N-ob (η .trans) d' .N-ob c) (lift r)) + -- ≡⟨ (λ i → lower ((η .trans .N-hom g i .N-ob c) (lift r))) ⟩ + -- lower ((N-ob (η .trans) d .N-ob c ⋆f + -- Prof*-o→Functor C D (bifCompF LiftF (Functor→Prof*-o C D G)) + -- .F-hom g .N-ob c) (lift r)) + -- ≡⟨ ((λ i → (Functor→Prof*-o C D G .Bif-idL i ⋆f + -- (Functor→Prof*-o C D G ⟪ g ⟫r)) + -- (lower (η .trans .N-ob d .N-ob c (lift r))))) ⟩ + -- (Functor→Prof*-o C D G ⟪ g ⟫r) + -- (lower (η .trans .N-ob d .N-ob c (lift r))) ∎ + -- }) , + -- λ d c → + -- (λ x → lower (η .nIso c .inv .N-ob d (lift x))) , + -- (λ x i → lower ((η .nIso c .sec i .N-ob d) (lift x))) , + -- (λ x i → lower((η .nIso c .ret i .N-ob d) (lift x))) + + -- open NatIso + -- open NatTrans + -- open isIsoC + + -- -- -- PshFunctorRepresentation → ParamUnivElt + -- -- PshFunctorRepresentation→ParamUnivElt : PshFunctorRepresentation → + -- -- ParamUnivElt + -- -- PshFunctorRepresentation→ParamUnivElt (G , η) = (λ c → + -- -- let R⟅-,c⟆ = (pAppR R c) in + -- -- let η⁻¹ = symNatIso η in + -- -- record { + -- -- vertex = (G ⟅ c ⟆) ; + -- -- element = lower ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id))) ; + -- -- universal = record { + -- -- coinduction = λ {d} ϕ → lower ((η .trans .N-ob c .N-ob d) (lift ϕ)); + -- -- commutes = (λ {d} ϕ → + -- -- let coindϕ = (lower ((η .trans .N-ob c .N-ob d) (lift ϕ))) in + -- -- lower (((LiftF ∘F R⟅-,c⟆) ⟪ coindϕ ⟫) + -- -- ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id)))) + -- -- ≡⟨ (λ i → lower (((LiftF ∘Fb R ) .Bif-idR (~ i)) + -- -- (((LiftF ∘Fb R ) .Bif-homL coindϕ c) + -- -- ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id)))))) ⟩ + -- -- lower ((((Prof*-o→Functor C D ((LiftF {ℓS}{ℓD'}) ∘Fb R )) ⟅ c ⟆) + -- -- ⟪ coindϕ ⟫) ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id)))) + -- -- ≡⟨ (λ i → lower ((((η⁻¹ .trans .N-ob c .N-hom coindϕ) (~ i)) + -- -- (lift (D .id))))) ⟩ + -- -- lower ((η⁻¹ .trans .N-ob c .N-ob d) + -- -- (((Bifunctor→Functor ((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D))) + -- -- ⟪ coindϕ , G ⟪ C .id ⟫ ⟫) (lift (D .id)))) + -- -- ≡⟨ ( λ i → lower ((η⁻¹ .trans .N-ob c .N-ob d) + -- -- (((Bifunctor→Functor ((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D))) + -- -- ⟪ coindϕ , G .F-id (i) ⟫) (lift (D .id))))) ⟩ + -- -- lower ((η⁻¹ .trans .N-ob c .N-ob d) + -- -- (((Bifunctor→Functor ((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D))) + -- -- ⟪ coindϕ , D .id ⟫) (lift (D .id)))) + -- -- ≡⟨ (λ i → + -- -- lower ((η⁻¹ .trans .N-ob c .N-ob d) + -- -- ((((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D)) .Bif-idR (i)) + -- -- ((((LiftF {ℓD'}{ℓS}) ∘Fb (HomBif D)) .Bif-homL coindϕ + -- -- (G ⟅ c ⟆)) (lift (D .id)))) + -- -- ) + -- -- ) ⟩ + -- -- lower ((η⁻¹ .trans .N-ob c .N-ob d) (lift (coindϕ ⋆⟨ D ⟩ (D .id)))) + -- -- ≡⟨ (λ i → lower ((η⁻¹ .trans .N-ob c .N-ob d) + -- -- (lift (D .⋆IdR coindϕ (i))))) ⟩ + -- -- lower ((η⁻¹ .trans .N-ob c .N-ob d) (lift (coindϕ))) + -- -- ≡⟨ (λ i → lower ((((η .nIso c .ret) (i)) .N-ob d) (lift ϕ))) ⟩ + -- -- ϕ ∎) ; + -- -- is-uniq = + -- -- λ {d} ϕ f ε⋆f≡ϕ → + -- -- let coindϕ = (lower ((η .trans .N-ob c .N-ob d) (lift ϕ))) in + -- -- f + -- -- ≡⟨ sym (D .⋆IdR f) ⟩ + -- -- (f ⋆⟨ D ⟩ D .id) + -- -- ≡⟨ (λ i → (((HomBif D) .Bif-idR (~ i)) + -- -- (((HomBif D) .Bif-homL f (G ⟅ c ⟆)) (D .id)))) ⟩ + -- -- (((Bifunctor→Functor (HomBif D)) ⟪ f , D .id ⟫) (D .id)) + -- -- ≡⟨ (λ i → (((Bifunctor→Functor (HomBif D)) + -- -- ⟪ f , G .F-id (~ i) ⟫) (D .id))) ⟩ + -- -- (((Bifunctor→Functor (HomBif D)) ⟪ f , G ⟪ C .id ⟫ ⟫) (D .id)) + -- -- ≡⟨ (λ i → lower(((η .nIso c .sec) (~ i) .N-ob d) + -- -- (lift (((Bifunctor→Functor (HomBif D)) + -- -- ⟪ f , G ⟪ C .id ⟫ ⟫) (D .id))))) ⟩ + -- -- lower ((η .trans .N-ob c .N-ob d) + -- -- ((η⁻¹ .trans .N-ob c .N-ob d) + -- -- (lift (((Bifunctor→Functor (HomBif D)) + -- -- ⟪ f , G ⟪ C .id ⟫ ⟫) (D .id))))) + -- -- ≡⟨ (λ i → lower ((η .trans .N-ob c .N-ob d) + -- -- (((η⁻¹ .trans .N-ob c .N-hom f) (i)) (lift (D .id))))) ⟩ + -- -- lower ((η .trans .N-ob c .N-ob d) + -- -- ((((Prof*-o→Functor C D ((LiftF {ℓS}{ℓD'}) ∘Fb R )) ⟅ c ⟆) ⟪ f ⟫) + -- -- ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id))))) + -- -- ≡⟨ ( λ i → lower ((η .trans .N-ob c .N-ob d) + -- -- (((LiftF ∘Fb R ) .Bif-idR (i)) (((LiftF ∘Fb R ) .Bif-homL f c) + -- -- ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id))))))) ⟩ + -- -- lower ((η .trans .N-ob c .N-ob d) (lift ((R⟅-,c⟆ ⟪ f ⟫) + -- -- (lower ((η⁻¹ .trans .N-ob c .N-ob (G ⟅ c ⟆)) (lift (D .id))))))) + -- -- ≡⟨ (λ i → (lower ((η .trans .N-ob c .N-ob d) + -- -- (lift (ε⋆f≡ϕ i))))) ⟩ + -- -- coindϕ ∎ + -- -- } + -- -- } + -- -- ) + + -- -- ParamUnivElt→Functor : ParamUnivElt → Functor C D + -- -- ParamUnivElt→Functor ues .F-ob c = ues c .vertex + -- -- ParamUnivElt→Functor ues .F-hom {x = c}{y = c'} f = + -- -- ues c' .universal .coinduction ((R ⟪ f ⟫r) (ues c .element)) + -- -- ParamUnivElt→Functor ues .F-id {x = c} = + -- -- cong (ues c .universal .coinduction) (λ i → R .Bif-idR i (ues c .element)) + -- -- ∙ sym (coinduction-elt (ues c .universal)) + -- -- ParamUnivElt→Functor ues .F-seq {x = c}{y = c'}{z = c''} f g = + -- -- -- Both sides are ≡ to R .Bif-homR (ues c .vertex) g + -- -- -- (R .Bif-homR (ues c .vertex) f (ues c .element)) + -- -- cong (ues c'' .universal .coinduction) + -- -- ((λ i → R .Bif-seqR f g i (ues c .element))) + -- -- ∙ cong (coinduction (ues c'' .universal)) + -- -- ( cong (R .Bif-homR (ues c .vertex) g) + -- -- (sym (ues c' .universal .commutes _)) + -- -- ∙ (λ i → R .Bif-assoc (ues c' .universal .coinduction ((R ⟪ f ⟫r) + -- -- (ues c .element))) g i (ues c' .element))) + -- -- ∙ sym (coinduction-natural (ues c'' .universal) _ _) + + -- -- -- ParamUnivElt → PshFunctorRepresentation + -- -- ParamUnivElt→PshFunctorRepresentation : ParamUnivElt → + -- -- PshFunctorRepresentation + -- -- ParamUnivElt→PshFunctorRepresentation ues = + -- -- (representing-functor , representing-nat-iso) where + -- -- representing-functor : Functor C D + -- -- representing-functor = ParamUnivElt→Functor ues + + -- -- rep-nat-iso-trans : (c : C .ob) → + -- -- NatTrans (Prof*-o→Functor C D (LiftF {ℓS}{ℓD'} ∘Fb R) .F-ob c) + -- -- (Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb + -- -- (Functor→Prof*-o C D representing-functor)) .F-ob c) + -- -- rep-nat-iso-trans c .N-ob d = + -- -- let R⟅-,c⟆ = (pAppR R c) in + -- -- (λ f → lift {ℓD'}{ℓS} ((ues c) .universal .coinduction {b = d} + -- -- (lower {ℓS}{ℓD'} f))) + -- -- rep-nat-iso-trans c .N-hom {d}{d'} ϕ = + -- -- let R⟅-,c⟆ = (pAppR R c) in + -- -- let εc = ues c .element in + -- -- let coind = (ues c) .universal .coinduction in + -- -- funExt λ x → + -- -- lift (coind (((Prof*-o→Functor C D R .F-ob c) ⟪ ϕ ⟫) (lower x))) + -- -- ≡⟨ ( λ i → lift (coind ((R .Bif-idR (i)) ((R .Bif-homL ϕ c) + -- -- (lower x))))) ⟩ + -- -- lift (coind (D [ (lower x) ∘ᴾ⟨ R⟅-,c⟆ ⟩ ϕ ] )) + -- -- ≡⟨ (λ i → lift ((coinduction-natural ((ues c) .universal) + -- -- (lower x) ϕ) (~ i))) ⟩ + -- -- lift ((coind (lower x)) ∘⟨ D ⟩ ϕ ) + -- -- ≡⟨ (λ i → lift (((HomBif D) .Bif-idR (~ i)) + -- -- (((HomBif D) .Bif-homL ϕ _) (coind (lower x)))) ) ⟩ + -- -- lift (((Bifunctor→Functor (HomBif D)) ⟪ ϕ , D .id ⟫ ) (coind (lower x))) + -- -- ≡⟨ (λ i → lift (((Bifunctor→Functor (HomBif D)) + -- -- ⟪ ϕ , representing-functor .F-id (~ i) ⟫ ) (coind (lower x)))) ⟩ + -- -- lift (((Bifunctor→Functor (HomBif D)) + -- -- ⟪ ϕ , representing-functor ⟪ C . id ⟫ ⟫ ) (coind (lower x))) ∎ + + -- -- representing-nat-iso : NatIso + -- -- (Prof*-o→Functor C D (LiftF {ℓS}{ℓD'} ∘Fb R)) + -- -- (Prof*-o→Functor C D (LiftF {ℓD'}{ℓS} ∘Fb + -- -- (Functor→Prof*-o C D representing-functor))) + -- -- representing-nat-iso .trans .N-ob c = rep-nat-iso-trans c + -- -- representing-nat-iso .trans .N-hom {x}{y} ψ = + -- -- let R⟅-,x⟆ = (pAppR R x) in + -- -- let R⟅-,y⟆ = (pAppR R y) in + -- -- let εy = ues y .element in + -- -- let εx = ues x .element in + -- -- let coindx = ues x .universal .coinduction in + -- -- let coindy = ues y .universal .coinduction in + -- -- makeNatTransPath (funExt (λ d → funExt (λ α → + -- -- lift (coindy (((Bifunctor→Functor R) ⟪ D .id , ψ ⟫) (lower α))) + -- -- ≡⟨ (λ i → lift (coindy + -- -- (R .Bif-homR _ ψ ((R .Bif-idL (i)) (lower α))))) ⟩ + -- -- lift (coindy (R .Bif-homR _ ψ (lower α))) + -- -- ≡⟨ ( λ i → lift (ues y .universal .is-uniq + -- -- (R .Bif-homR _ ψ (lower α)) + -- -- ((coindx (lower α)) ⋆⟨ D ⟩ (representing-functor ⟪ ψ ⟫)) + -- -- ( + -- -- ( + -- -- D [ εy ∘ᴾ⟨ R⟅-,y⟆ ⟩ (coindy ((R .Bif-homR _ ψ) εx) ∘⟨ D ⟩ + -- -- (coindx (lower α))) ] + -- -- ≡⟨ (λ i → D [ + -- -- εy ∘ᴾ⟨ R⟅-,y⟆ ⟩ ((coinduction-natural (ues y .universal) + -- -- ((R .Bif-homR _ ψ) εx) (coindx (lower α))) i)] ) ⟩ + -- -- D [ εy ∘ᴾ⟨ R⟅-,y⟆ ⟩ + -- -- coindy ( D [ ((R .Bif-homR _ ψ) εx) ∘ᴾ⟨ R⟅-,y⟆ ⟩ + -- -- (coindx (lower α)) ]) ] + -- -- ≡⟨ ues y .universal .commutes + -- -- (D [ ((R .Bif-homR _ ψ) εx) ∘ᴾ⟨ R⟅-,y⟆ ⟩ + -- -- (coindx (lower α)) ]) ⟩ + -- -- D [ ((R .Bif-homR _ ψ) εx) ∘ᴾ⟨ R⟅-,y⟆ ⟩ (coindx (lower α)) ] + -- -- ≡⟨ (λ i → ((R .Bif-assoc (coindx (lower α)) ψ) (~ i)) εx) ⟩ + -- -- (R .Bif-homR _ ψ) (D [ εx ∘ᴾ⟨ R⟅-,x⟆ ⟩ (coindx (lower α)) ]) + -- -- ≡⟨ (λ i → (R .Bif-homR _ ψ) + -- -- (ues x .universal .commutes (lower α) (i))) ⟩ + -- -- (R .Bif-homR _ ψ (lower α)) ∎ + -- -- ) + -- -- ) + -- -- (~ i))) ⟩ + -- -- lift ((coindx (lower α)) ⋆⟨ D ⟩ (representing-functor ⟪ ψ ⟫)) + -- -- ≡⟨ (λ i → lift ((HomBif D) .Bif-homR _ (representing-functor ⟪ ψ ⟫) + -- -- (((HomBif D) .Bif-idL (~ i)) (coindx (lower α))))) ⟩ + -- -- lift (((Bifunctor→Functor (HomBif D)) ⟪ D .id , + -- -- representing-functor ⟪ ψ ⟫ ⟫) (coindx (lower α))) ∎ + + -- -- ))) + -- -- representing-nat-iso .nIso c .inv .N-ob d = + -- -- let εc = ues c .element in + -- -- let R⟅-,c⟆ = (pAppR R c) in + -- -- λ f → lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (lower f) ]) + -- -- representing-nat-iso .nIso c .inv .N-hom {d}{d'} ϕ = + -- -- let εc = ues c .element in + -- -- let R⟅-,c⟆ =(pAppR R c) in + -- -- funExt λ x → + -- -- lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ ((Bifunctor→Functor (HomBif D)) + -- -- ⟪ ϕ , representing-functor ⟪ C .id ⟫ ⟫) (lower x) ]) + -- -- ≡⟨ (λ i → lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ ((Bifunctor→Functor (HomBif D)) + -- -- ⟪ ϕ , representing-functor .F-id i ⟫) (lower x) ])) ⟩ + -- -- lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ ((Bifunctor→Functor (HomBif D)) + -- -- ⟪ ϕ , D .id ⟫ ) (lower x) ]) + -- -- ≡⟨ (λ i → lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ ((HomBif D) .Bif-idR (i) + -- -- (((HomBif D) .Bif-homL ϕ _) (lower x))) ])) ⟩ + -- -- lift (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (ϕ ⋆⟨ D ⟩ (lower x)) ]) + -- -- ≡⟨ (λ i → lift (((R⟅-,c⟆ .F-seq (lower x) ϕ) i) εc)) ⟩ + -- -- lift ((R .Bif-homL ϕ _) (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (lower x) ])) + -- -- ≡⟨ (λ i → lift ((R .Bif-idR (~ i)) ((R .Bif-homL ϕ _) + -- -- (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (lower x) ])))) ⟩ + -- -- lift (((Bifunctor→Functor R) ⟪ ϕ , C .id ⟫) + -- -- (D [ εc ∘ᴾ⟨ R⟅-,c⟆ ⟩ (lower x) ])) ∎ + + -- -- representing-nat-iso .nIso c .sec = + -- -- let R⟅-,c⟆ = (pAppR R c) in + -- -- makeNatTransPath (funExt λ d → funExt λ x → (λ i → + -- -- lift ((η-expansion ((ues c) .universal) (lower x)) (~ i))) ) + -- -- representing-nat-iso .nIso c .ret = + -- -- let R⟅-,c⟆ = (pAppR R c) in + -- -- makeNatTransPath (funExt λ d → funExt λ x → (λ i → + -- -- lift (((ues c) .universal .commutes (lower x)) i))) + + -- -- -- ParamUniversalElement → ParamUnivElt + -- -- ParamUniversalElement→ParamUnivElt : ParamUniversalElement → ParamUnivElt + -- -- ParamUniversalElement→ParamUnivElt U c = + -- -- UniversalElement→UnivElt D (pAppR R c) (U c) + + -- -- -- ParamUnivElt → ParamUniversalElement + -- -- ParamUnivElt→ParamUniversalElement : ParamUnivElt → ParamUniversalElement + -- -- ParamUnivElt→ParamUniversalElement U c = + -- -- UnivElt→UniversalElement D (pAppR R c) (U c) + + -- -- {- + -- -- We have now given maps + -- -- ProfRepresentation ⇔ PshFunctorRepresentation + -- -- PshFunctorRepresentation ⇔ ParamUnivElt + -- -- ParamUnivElt ⇔ ParamUniversalElement + + -- -- For convenience, + -- -- below we also stitch these together to give all pairwise maps. + -- -- -} + + -- -- -- ProfRepresentation → ParamUnivElt + -- -- ProfRepresentation→ParamUnivElt : ProfRepresentation → ParamUnivElt + -- -- ProfRepresentation→ParamUnivElt R = + -- -- PshFunctorRepresentation→ParamUnivElt + -- -- (ProfRepresentation→PshFunctorRepresentation R) + + -- -- -- ProfRepresentation → ParamUniversalElement + -- -- ProfRepresentation→ParamUniversalElement : ProfRepresentation → + -- -- ParamUniversalElement + -- -- ProfRepresentation→ParamUniversalElement R = + -- -- ParamUnivElt→ParamUniversalElement (ProfRepresentation→ParamUnivElt R) + + -- -- -- PshFunctorRepresentation → ParamUniversalElement + -- -- PshFunctorRepresentation→ParamUniversalElement : PshFunctorRepresentation → + -- -- ParamUniversalElement + -- -- PshFunctorRepresentation→ParamUniversalElement R = + -- -- ParamUnivElt→ParamUniversalElement (PshFunctorRepresentation→ParamUnivElt R) + + -- -- -- ParamUnivElt → ProfRepresentation + -- -- ParamUnivElt→ProfRepresentation : ParamUnivElt → ProfRepresentation + -- -- ParamUnivElt→ProfRepresentation U = + -- -- PshFunctorRepresentation→ProfRepresentation + -- -- (ParamUnivElt→PshFunctorRepresentation U) + + -- -- -- ParamUniversalElement → ProfRepresentation + -- -- ParamUniversalElement→ProfRepresentation : ParamUniversalElement → + -- -- ProfRepresentation + -- -- ParamUniversalElement→ProfRepresentation U = + -- -- ParamUnivElt→ProfRepresentation (ParamUniversalElement→ParamUnivElt U) + + -- -- -- ParamUniversalElement → PshFunctorRepresentation + -- -- ParamUniversalElement→PshFunctorRepresentation : ParamUniversalElement → + -- -- PshFunctorRepresentation + -- -- ParamUniversalElement→PshFunctorRepresentation U = + -- -- ParamUnivElt→PshFunctorRepresentation (ParamUniversalElement→ParamUnivElt U) diff --git a/Cubical/Categories/Yoneda/More.agda b/Cubical/Categories/Yoneda/More.agda index 103dffde..315e3bcc 100644 --- a/Cubical/Categories/Yoneda/More.agda +++ b/Cubical/Categories/Yoneda/More.agda @@ -34,87 +34,6 @@ open NatTransP open Functor open Iso --- 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 - -- But this one is nice because its action on functors is -- *definitionally* equal to the definition used in -- the formulation of the Yoneda lemma diff --git a/Cubical/Data/Graph/Properties.agda b/Cubical/Data/Graph/Properties.agda deleted file mode 100644 index 810051c6..00000000 --- a/Cubical/Data/Graph/Properties.agda +++ /dev/null @@ -1,32 +0,0 @@ --- Free category over a directed graph/quiver -{-# OPTIONS --safe #-} - -module Cubical.Data.Graph.Properties where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.HLevels -open import Cubical.Data.Graph -open import Cubical.Categories.Category.Base - - -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 diff --git a/Cubical/Foundations/Isomorphism/More.agda b/Cubical/Foundations/Isomorphism/More.agda new file mode 100644 index 00000000..172ebb20 --- /dev/null +++ b/Cubical/Foundations/Isomorphism/More.agda @@ -0,0 +1,22 @@ +{-# OPTIONS --safe #-} +module Cubical.Foundations.Isomorphism.More where + +open import Cubical.Core.Everything + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv.Base +open import Cubical.Foundations.Isomorphism + +private + variable + ℓ ℓ' : Level + A B C : Type ℓ + +isoToIsIso : {f : A → B} → isIso f → Iso A B +isoToIsIso {f = f} fIsIso .Iso.fun = f +isoToIsIso fIsIso .Iso.inv = fIsIso .fst +isoToIsIso fIsIso .Iso.rightInv = fIsIso .snd .fst +isoToIsIso fIsIso .Iso.leftInv = fIsIso .snd .snd + +isIsoToIsEquiv : {f : A → B} → isIso f → isEquiv f +isIsoToIsEquiv fIsIso = isoToIsEquiv (isoToIsIso fIsIso) diff --git a/Cubical/Tactics/CategorySolver/Examples.agda b/Cubical/Tactics/CategorySolver/Examples.agda deleted file mode 100644 index 15eb837f..00000000 --- a/Cubical/Tactics/CategorySolver/Examples.agda +++ /dev/null @@ -1,35 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Tactics.CategorySolver.Examples where - -open import Cubical.Categories.Category -open import Cubical.Foundations.Prelude -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 deleted file mode 100644 index 48926857..00000000 --- a/Cubical/Tactics/CategorySolver/Reflection.agda +++ /dev/null @@ -1,71 +0,0 @@ -{-# 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.Categories.Category -open import Cubical.Categories.Constructions.Free.General -open import Cubical.Tactics.CategorySolver.Solver -open import Cubical.Tactics.Reflection - -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∷ [])) - - -- This seems really hacky tbh - pattern “comp” f g = - def (quote comp') (category-args (_ h∷ _ h∷ _ h∷ g v∷ f 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 (“comp” f g) = - con (quote FreeCategory._⋆ₑ_) - (buildExpression f v∷ buildExpression g v∷ []) - buildExpression f = con (quote FreeCategory.↑_) (f v∷ []) - - solve-macro : Bool - → Term -- ^ The term denoting the category - → Term -- ^ The hole whose goal should be an equality - -- between morphisms in the category - → TC Unit - solve-macro b category = - equation-solver - (quote Category.id ∷ quote Category._⋆_ ∷ quote comp' ∷ []) mk-call b 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 false - - solveCatDebug! : Term → Term → TC _ - solveCatDebug! = ReflectionSolver.solve-macro true diff --git a/Cubical/Tactics/CategorySolver/Solver.agda b/Cubical/Tactics/CategorySolver/Solver.agda deleted file mode 100644 index 603a2792..00000000 --- a/Cubical/Tactics/CategorySolver/Solver.agda +++ /dev/null @@ -1,54 +0,0 @@ -{-# OPTIONS --safe --lossy-unification #-} -module Cubical.Tactics.CategorySolver.Solver where - -open import Cubical.Foundations.Prelude -open import Cubical.Categories.Category -open import Cubical.Categories.Functor.Base -open import Cubical.Categories.Instances.Sets - -open import Cubical.Categories.Constructions.Free.General -open import Cubical.Categories.Constructions.Free.UnderlyingGraph -open import Cubical.Categories.Constructions.Power - -private - variable - ℓ ℓ' : Level -open Category -open Functor - -module Eval (𝓒 : Category ℓ ℓ') where - -- Semantics in 𝓒 itself, tautologically - open FreeCategory (Ugr 𝓒) - sem𝓒 = ε {𝓒 = 𝓒} - ⟦_⟧c = sem𝓒 .F-hom - 𝓟 = PowerCategory (𝓒 .ob) (SET (ℓ-max ℓ ℓ')) - 𝓘 : Functor FreeCat 𝓟 - 𝓘 = PseudoYoneda {C = FreeCat} - - -- Semantics in 𝓟o 𝓒, interpreting fun symbols using Yoneda - module YoSem = Semantics 𝓟 (𝓘 ∘Interp η) - ⟦_⟧yo = YoSem.sem .F-hom - - -- | Evaluate by taking the semantics in 𝓟 𝓒 and - -- | use the Yoneda lemma to extract a morphism in 𝓒. - eval : ∀ {A B} → FreeCat [ A , B ] → _ - eval {A}{B} e = ⟦ e ⟧yo - - Yo-YoSem-agree : 𝓘 ≡ YoSem.sem - Yo-YoSem-agree = YoSem.sem-uniq refl - - -- | Eval agrees with the tautological semantics - 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 (Ugr 𝓒) [ 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 deleted file mode 100644 index c5c50697..00000000 --- a/Cubical/Tactics/FunctorSolver/Examples.agda +++ /dev/null @@ -1,36 +0,0 @@ -{-# OPTIONS --safe #-} -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 ∘⟨ C ⟩ C .id ⟫ - _ = solveFunctor! C D F diff --git a/Cubical/Tactics/FunctorSolver/Reflection.agda b/Cubical/Tactics/FunctorSolver/Reflection.agda deleted file mode 100644 index 3041794e..00000000 --- a/Cubical/Tactics/FunctorSolver/Reflection.agda +++ /dev/null @@ -1,90 +0,0 @@ -{-# 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.Categories.Category -open import Cubical.Categories.Functor -open import Cubical.Categories.Constructions.Free.General -open import Cubical.Categories.Constructions.Free.Functor -open import Cubical.Tactics.FunctorSolver.Solver -open import Cubical.Tactics.Reflection - -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 deleted file mode 100644 index 2f56d52e..00000000 --- a/Cubical/Tactics/FunctorSolver/Solver.agda +++ /dev/null @@ -1,68 +0,0 @@ -{-# OPTIONS --safe --lossy-unification #-} -module Cubical.Tactics.FunctorSolver.Solver where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Path -open import Cubical.Foundations.Id renaming (refl to reflId) hiding (_∙_) -open import Cubical.Foundations.GroupoidLaws -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Function renaming (_∘_ to _∘f_) -open import Cubical.Categories.Category -open import Cubical.Categories.Functor renaming (Id to IdF) -open import Cubical.Categories.NaturalTransformation -open import Cubical.Data.Graph.Base -open import Cubical.Categories.Presheaf -open import Cubical.Categories.Instances.Sets - -open import Cubical.Categories.Constructions.Free.Functor -open import Cubical.Categories.Constructions.Free.UnderlyingGraph -open import Cubical.Data.Graph.Properties -open import Cubical.Categories.Yoneda.More -open import Cubical.Categories.NaturalTransformation.More -open import Cubical.Tactics.CategorySolver.Reflection - -open import Cubical.Categories.Constructions.Power - -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 (Ugr 𝓒) (Ugr 𝓓) (𝓕 .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 reflId - module YoSem = Semantics {𝓒 = 𝓟} {𝓓 = 𝓟} {𝓕 = IdF} - (Uhom (PsYo ∘F Free𝓕) ∘GrHom η𝓒) - (Uhom PsYo ∘GrHom η𝓓) - reflId - - 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 (symPath (lUnit (idToPath reflId)) - ∙ idToPathRefl - ∙ 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 = congPath (TautoSem.semH .F-hom) - (isFaithfulPseudoYoneda _ _ _ _ lem) where - lem : Path _ (PsYo ⟪ e ⟫) (PsYo ⟪ e' ⟫) - lem = transportPath (λ 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 deleted file mode 100644 index cbb67679..00000000 --- a/Cubical/Tactics/Reflection.agda +++ /dev/null @@ -1,116 +0,0 @@ -{-# 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 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.Categories.Category -open import Cubical.Categories.Constructions.Free.General -open import Cubical.Tactics.CategorySolver.Solver - -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 ∷ - strErr "\nIn the call\n " ∷ - termErr call ∷ [])))))) diff --git a/Makefile b/Makefile index f1e09791..1a8292df 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,7 @@ AGDA = agda FIX_WHITESPACE = fix-whitespace # Finds all .agda files in the current directory and subdirectories -AGDA_FILES = $(shell find . -name "*.agda") +AGDA_FILES = $(shell find Cubical -name "*.agda") # The targets are the .agdai files corresponding to the .agda files AGDAI_FILES = $(AGDA_FILES:.agda=.agdai)