succinct definition of a simple category with families

Cubical/Categories/Instances/Sets/More.agda

@@ -4,9 +4,13 @@ module Cubical.Categories.Instances.Sets.More where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+open import Cubical.Data.Sigma
+
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Constructions.BinProduct
 
 private
   variable
@@ -20,3 +24,8 @@ LiftF .F-hom f x = lift (f (x .lower))
 LiftF .F-id = refl
 LiftF .F-seq f g = funExt λ x → 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

NaturalModels/SimpleCwF.agda

@@ -0,0 +1,28 @@
+module NaturalModels.SimpleCwF where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Instances.Sets.More
+open import Cubical.Categories.Limits.Terminal
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Presheaf.Representable
+
+open Category
+SCwF : (ℓ ℓ' ℓ'' ℓ''' : Level)
+     → Type (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ')) (ℓ-suc ℓ'')) (ℓ-suc ℓ'''))
+SCwF ℓ ℓ' ℓ'' ℓ''' =
+  -- The category of contexts and substitutions
+  Σ[ C ∈ Category ℓ ℓ' ]
+  -- With a terminal object (empty context)
+  Terminal C ×
+  -- A type of syntactic types
+  (Σ[ Ty ∈ Type ℓ'' ]
+  -- A presheaf of terms for each type
+  Σ[ Tm ∈ (∀ (A : Ty) → Presheaf C ℓ''') ]
+  -- Such that the base category has products with terms (context extension)
+  (∀ (Γ : C .ob) (A : Ty)
+  → UnivElt C (×Sets ∘F (LiftF {ℓ' = ℓ'''} ∘F ((C [-, Γ ])) ,F LiftF {ℓ' = ℓ'} ∘F Tm A))))