Category of elements as a wild functor to CAT. (#1160)

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.agda

@@ -19,7 +19,6 @@ open import Cubical.Categories.Isomorphism
 import      Cubical.Categories.Morphism as Morphism
 
 
-
 module Cubical.Categories.Constructions.Elements where
 
 -- some issues
@@ -81,6 +80,11 @@ module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
           p2 = snd ((∫ F) ._⋆_ f' ((∫ F) ._⋆_ {o1} {o2} {o3} g' h'))
     (∫ F) .isSetHom {x} {y} = isSetΣSndProp (C .isSetHom) λ _ → (F ⟅ fst y ⟆) .snd _ _
 
+    ElementHom≡ : ∀ {ℓS} (F : Functor C (SET ℓS)) → {c,f c',f' : Element F}
+      → {χ1,ef1 χ2,ef2 : (∫ F) [ c,f , c',f' ]} → (fst χ1,ef1 ≡ fst χ2,ef2) → (χ1,ef1 ≡ χ2,ef2)
+    ElementHom≡ F {c1 , f1} {c2 , f2} {χ1 , ef1} {χ2 , ef2} eχ = cong₂ _,_ eχ
+      (fst (isOfHLevelPathP' 0 (snd (F ⟅ c2 ⟆) _ _) ef1 ef2))
+
     ForgetElements : ∀ {ℓS} → (F : Functor C (SET ℓS)) → Functor (∫ F) C
     F-ob (ForgetElements F) = fst
     F-hom (ForgetElements F) = fst

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/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