§ 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

• For the Metatheory of Type Theory, Internal Sconing Is Enough
• Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus