update to cubical HEAD (#39)

maxsnew · Jul 14, 2023 · d7a0db1 · d7a0db1
1 parent 38cd7d4
commit d7a0db1
Show file tree

Hide file tree

Showing 42 changed files with 997 additions and 3,196 deletions.
diff --git 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
@@ -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
@@ -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
diff --git 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
@@ -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
@@ -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
@@ -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
diff --git a/...tegories/Constructions/Free/Category.agda → ...s/Constructions/Free/Category/Quiver.agda b/...tegories/Constructions/Free/Category.agda → ...s/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