Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
In the first sentence
Suppose we have a fibration p:ℰ→ℬ, representing type families (living in the fibers of ℰ) indexed by contexts (living in ℬ).
probably “fibration” means “Grothendieck fibration”? (I have now hyperlinked it as such). But then referring to this as a “type family” is unusual – unless maybe you want to speak of directed type theory?
I think this should be clarified.
Oh, I see. So I misread what you mean. (Haven’t take much time with the entry, admittedly).
But then lets’ say this in the entry: “whose objects are type families”.
And add a link to category with families! (or whatever it may be)
Thanks. So I have appended pointer to categorical semantics of dependent types.
I have made the link to “fibered terminal object” that you request here point to fibered limit.
But now I realize it may not be the pointer you intend(?):
In the usual language a fibered category p:E→B has a fibered terminal object if (e.g. p. 6 here) E and B have terminal objects and p preserves the terminal object. To get from there to the condition you state one needs an extra assumption, I suppose, such as the base change preserving limits, hence such as the fibration being a bifibration. No? Maybe you could expand on this point in the entry.
1 to 10 of 10