Merge branch 'master' into const-inst

Cubical/Categories/Category.agda

@@ -1,17 +1,17 @@
 {-
   Definition of various kinds of categories.
 
-  This library follows the UniMath terminology, that is:
+  This library partially follows the UniMath terminology:
 
   Concept              Ob C   Hom C  Univalence
 
-  Precategory          Type   Type   No
+  Wild Category        Type   Type   No           (called precategory in UniMath)
   Category             Type   Set    No
   Univalent Category   Type   Set    Yes
 
   The most useful notion is Category and the library is hence based on
-  them. If one needs precategories then they can be found in
-  Cubical.Categories.Category.Precategory
+  them. If one needs wild categories then they can be found in
+  Cubical.WildCat (so it's not considered part of the Categories sublibrary!)
 
 -}
 {-# OPTIONS --safe #-}

Cubical/Categories/Constructions/Elements/Properties.agda

@@ -0,0 +1,52 @@
+{-# OPTIONS --safe #-}
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Categories.Category
+open Category
+open import Cubical.Categories.Functor
+open Functor
+open import Cubical.Categories.NaturalTransformation
+open NatTrans
+open import Cubical.Categories.Instances.Functors
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Constructions.Elements
+open Covariant
+
+open import Cubical.WildCat.Functor
+open import Cubical.WildCat.Instances.Categories
+open import Cubical.WildCat.Instances.NonWild
+
+module Cubical.Categories.Constructions.Elements.Properties where
+
+variable
+  ℓC ℓC' ℓD ℓD' ℓS : Level
+  C : Category ℓC ℓC'
+  D : Category ℓD ℓD'
+
+∫-hom : ∀ {F G : Functor C (SET ℓS)} → NatTrans F G → Functor (∫ F) (∫ G)
+Functor.F-ob (∫-hom ν) (c , f) = c , N-ob ν c f
+Functor.F-hom (∫-hom ν) {c1 , f1} {c2 , f2} (χ , ef) = χ , sym (funExt⁻ (N-hom ν χ) f1) ∙ cong (N-ob ν c2) ef
+Functor.F-id (∫-hom {G = G} ν) {c , f} = ElementHom≡ G refl
+Functor.F-seq (∫-hom {G = G} ν) {c1 , f1} {c2 , f2} {c3 , f3} (χ12 , ef12) (χ23 , ef23) =
+  ElementHom≡ G refl
+
+∫-id : ∀ (F : Functor C (SET ℓS)) → ∫-hom (idTrans F) ≡ Id
+∫-id F = Functor≡
+  (λ _ → refl)
+  λ {(c1 , f1)} {(c2 , f2)} (χ , ef) → ElementHom≡ F refl
+
+∫-seq : ∀ {C : Category ℓC ℓC'} {F G H : Functor C (SET ℓS)} → (μ : NatTrans F G) → (ν : NatTrans G H)
+  → ∫-hom (seqTrans μ ν) ≡ funcComp (∫-hom ν) (∫-hom μ)
+∫-seq {H = H} μ ν = Functor≡
+  (λ _ → refl)
+  λ {(c1 , f1)} {(c2 , f2)} (χ , ef) → ElementHom≡ H refl
+
+module _ (C : Category ℓC ℓC') (ℓS : Level) where
+
+  ElementsWildFunctor : WildFunctor (AsWildCat (FUNCTOR C (SET ℓS))) (CatWildCat (ℓ-max ℓC ℓS) (ℓ-max ℓC' ℓS))
+  WildFunctor.F-ob ElementsWildFunctor = ∫_
+  WildFunctor.F-hom ElementsWildFunctor = ∫-hom
+  WildFunctor.F-id ElementsWildFunctor {F} = ∫-id F
+  WildFunctor.F-seq ElementsWildFunctor μ ν = ∫-seq μ ν

Cubical/Categories/Instances/Elements.agda

@@ -12,14 +12,13 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category
-import      Cubical.Categories.Instances.Slice.Base as Slice
+import      Cubical.Categories.Constructions.Slice.Base as Slice
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Isomorphism
 import      Cubical.Categories.Morphism as Morphism
 
 
-
 module Cubical.Categories.Instances.Elements where
 
 -- some issues

Cubical/WildCat/Instances/NonWild.agda

@@ -0,0 +1,37 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.WildCat.Instances.NonWild where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor.Base
+
+open import Cubical.WildCat.Base
+open import Cubical.WildCat.Functor
+
+module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
+
+  open WildCat
+  open Category
+
+  AsWildCat : WildCat ℓ ℓ'
+  ob AsWildCat = ob C
+  Hom[_,_] AsWildCat = Hom[_,_] C
+  id AsWildCat = id C
+  _⋆_ AsWildCat = _⋆_ C
+  ⋆IdL AsWildCat = ⋆IdL C
+  ⋆IdR AsWildCat = ⋆IdR C
+  ⋆Assoc AsWildCat = ⋆Assoc C
+
+
+module _ {ℓC ℓC' ℓD ℓD' : Level} {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) where
+
+  open Functor
+  open WildFunctor
+
+  AsWildFunctor : WildFunctor (AsWildCat C) (AsWildCat D)
+  F-ob AsWildFunctor = F-ob F
+  F-hom AsWildFunctor = F-hom F
+  F-id AsWildFunctor = F-id F
+  F-seq AsWildFunctor = F-seq F