I am currently trying to understand how to formalize homotopy type theory in Church-style as proposed in the second appendix of the HoTT book.
How am I supposed to interpret the constructors of positive types as the $\sum$- type, the coproduct type, the natural numbers or the identity type?
Is $\mathrm{inl}$ in the second appendix a meta-theoretic notion? If so, would this mean that $\mathrm{inl}$ isn't a term of our formal theory and we cannot construct a function $\lambda (a:A).\mathrm{inl}(a):A\to A+B$? I'm just wondering as I always pictured the constructors of the coproduct as injections.