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 [Cop,Set].
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 X on C, XΠ is given on objects by XΠ(Γ)=ΣA:Ty(Γ)X(Γ,A), i.e., it is the presheaf of “Xs 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 T is a Π-type Π(x:A).B, then by inductive hypothesis, [[A]]Vtype:TmV⇀Ty, wlog. we can pick x fresh for V, that is x∉V and [[B]]V∪{x}type:TmV∪{x}⇀Ty. By restricting the domain of [[B]]V∪{x}type and currying we get F:TmV⇀Ty𝒜 where 𝒜 is the fiber of [[A]]Vtype along of:Tm→Ty (when this makes sense, F being undefined otherwise). Then
[[Π(x:A).B]]Vtype=Π∘⟨[[A]]Vtype,F⟩:TmV⇀TyI think it also works rather well for λ and App, my only problem before starting to write the partial interpretation is that I have trouble with writing down a more precise definition of F 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 [Cop,Set].
Reformulating TyΠ and TmΠ 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 $Γ,x:A,f:Π(x:A)B⊢Appx:A.B(f,x):B$
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 PΠ:[Cop,Set]→[Cop,Set] is the composition of three functors. Firstly we have the pullback along Tm→1 usually denoted Tm*, then we have the right adjoint to pullback along of, which I will call ∏of and finally composition along Ty→1 giving us our functor PΠ. Then the Π-structure on a CwF is two maps λ and Π that satisfy the square.
1 to 9 of 9