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.
I think it would be best to give the definitions of this structure in as close a manner as possible to what we’ll want for the interpretation.
Im finding this hard to parse, its the same problem with Awodey’s paper too. Is this a difficult concept to grasp or to parse?
It makes somewhat more sense when expressed in the internal extensional type theory of .
It helped me to first take Proposition 5 in Awodey as the definition of the operation , and then revisit the concrete description as a polynomial functor.
That is that for a preasheaf on , is given on objects by , i.e., it is the presheaf of “s in an extended context”. Then the typing of and make a lot of sense and unwinding the pullback tells you that has type plus the laws.
Re #2 I think it matches rather closely :
For instance if is a -type , then by inductive hypothesis, , wlog. we can pick fresh for , that is and . By restricting the domain of and currying we get where is the fiber of along (when this makes sense, being undefined otherwise). Then
I think it also works rather well for and , my only problem before starting to write the partial interpretation is that I have trouble with writing down a more precise definition of above.
Yes, it’s pretty close, but I think it would match even more closely if we state the categorical definition using application and abstraction morphisms. E.g. I’m thinking of translating Definition 3.4.2.1 of the local universes paper into the language of .
Reformulating and using @maxsnew version that seems more understandable.
Re #7 I looked at the definition in that paper but I couldn’t come up with something that seemed better than the current one. Also I have the impression that providing a natural transformation for application correspond to giving eagerly the denotation of $$
How can this be phrased talking about the category of elements? This is some very confusing category theory.
If I am understanding correctly the functor is the composition of three functors. Firstly we have the pullback along usually denoted , then we have the right adjoint to pullback along , which I will call and finally composition along giving us our functor . Then the -structure on a CwF is two maps and that satisfy the square.
1 to 9 of 9