sketch of categorical semantics

what-is-an-intensional-model.org

+* Term Model
+
+** CBPV
+
+A judgmental cbpv model is
+
+1. A cartesian category 𝓒 of "pure functions"
+2. A subset of the objects of 𝓒 called the "value types"
+3. A 𝓟𝓒-enriched category 𝓔 of "linear functions", whose objects are
+   "computation types"
+4. 𝓟𝓒-enriched presheaf W on 𝓔
+
+Type structure:
+1. 𝓒 has product types if the value types are closed under products
+2. 𝓒 has pure function types if the vtypes are closed under exponentials
+3. 𝓒 has sum types if the value types are closed under *distributive*
+   coproducts
+4. 𝓒 has a ▹ type if for every A ∈ VType, the presheaf
+   P(Γ) = ▹ (𝓒 [ Γ , A ]) is representable
+5. 𝓒 has linear function types if every Hom_𝓔(B,B') is representable
+6. 𝓒 has thunks if every W B is representable
+
+Similarly:
+1. 𝓔 has function types if it has powers of 𝓒-types
+2. 𝓔 has returners if for every vtype A, the enriched covariant
+   presheaf Q(B)_Γ = W B (Γ × A) is (enriched) representable
+3. 𝓔 has product types if it has enriched products
+4. 𝓔 has
+This isn't quite right tho, because W needs to respect the powers...
+*** Alt
+
+A judgmental cbpv model is
+
+1. A cartesian category 𝓒 of "pure functions"
+2. A distinguished subset of 𝓒 objects called "value types"
+3. A 𝓟 𝓒-enriched category 𝓔 of "linear functions"
+4. A distinguished object W ∈ 𝓔 of "machines"
+5. A distinguished subset of 𝓔 objects called "computation types"
+
+** CBV/CBN
+
+Special cases:
+1. a judgmental cbv model is
+   - A cartesian category 𝓒
+   - A subset of types, which determines a 𝓟𝓒-enriched category 𝓣
+   - A 𝓟𝓒-enriched presheaf 𝓔 on 𝓣
+   - A 𝓟𝓒-enriched promonad structure on 𝓣 with underlying profunctor:
+     (𝓛 A B) Γ = 𝓔 B (Γ × A)
+
+   From this data, we can generate a cbpv model with 𝓒 as the
+   cartesian category and defining a "Kleisli" category whose objects
+   are 𝓣 + 1 with
+     (𝓔 (inl A) B) Γ = 𝓛 A B Γ
+     (𝓔 (inr *) B) Γ = 𝓔 Γ B
+
+   This can be generated for instance from
+   - A cartesian category 𝓒 and a strong monad T on 𝓒
+2. a judgmental cbn model is
+   - A cartesian category 𝓒
+   - a subset of types determining a wide subcategory 𝓣
+   - A subcategory? 𝓛 of 𝓣 of "linear" functions or should it be a
+     procomonad?
+
+   This can be generated for instance from a cartesian category 𝓒 and a (strong?) comonad W on 𝓒
+
+3. A cartesian category 𝓒 of contexts and "pure functions"
+4. Chosen subsets of the objects of 𝓒 called "types"
+5. For each type A ∈ Types, a presheaf Eff A ∈ 𝓟 𝓒
+   1. A natural element ret ∈ Y A ⇒ Eff A
+   2. A natural transformation bind ∈ (Y A ⇒ Eff B) ⇒ Eff A ⇒ Eff B
+   3. satisfying ...
+
+      
+* Relational Model
+
+To get a "relational" model, take the above and do it all internal to
+Cat. To make it more like relations, we should require it to be
+2-posetal (i.e. at most one 2-cell) and be fibrant (i.e., functions
+induce relations).
+
+This is all in the internal language of the topos of trees.
+
+An intensional cbv λ model with relations consists of:
+
+1. A double category 𝓒 that is cartesian, locally posetal and fibrant.
+2. A chosen subset of objects of 𝓒 called types.
+3. For each type A ∈ Types, a double presheaf  that is locally posetal and fibrant
+
+
+
+1. A cartesian locally posetal double category 𝓒.
+
+   Locally posetal means that there is at most one two cell of any
+   given framing.
+
+   Cartesian means it has finite products
+
+2. A locally posetal double category of types and effectful morphisms
+   𝓔
+
+   
+
+3. A locally posetal double profunctor Tm : 𝓒 o-* Eff
+
+