§ Notes on CwFs and categorical NbE
§ Fibered versus Indexed
- Fibered:
TM -> M. - Indexed:
(p : M) -> TpM.
§ Categories with Families
-
Ty: Ctx^op -> Set (map a context to the set of valid types in that context). -
Tm : (Γ : Ctx^op) -> Ty Γ -> Set (map a type to the set of inhabitants). - Most syntactic way of talking about categories.
§ Comprehension Categories
-
Ctx is a category of contexts. -
Ty is the category of types, which is fibered over the category of contexts. - Most semantic way of talking about categories.
§ Paper References