Logic within Type theory. Is there a rough academic consensus on how this should be done? I guess because of it's presence in several blogs on math and even physics, I've recently started to learn some type theory, often from people who know about it and from books which use it. I want to write down some personal notes, specifically about how mathematics is done in it, but I kind of have a problem in that there seem to be dozens of ways to implement logic in it and I don't even see which one is more canon than the other. "My work" so far consisting in collecting the ideas which I have encounter.
A rule like 
$$\frac{\Gamma\vdash a:P\hspace{1cm}\Gamma\vdash f:P\to Q}{\Gamma\vdash f(a):Q}$$
is essentially using the "if-then" idea three times at once. The vertical axis $\frac{foo}{bar}$ is used as for natural deduction, the $\vdash$ being substituted by implications $\implies$. Other times we seem to do proof theory with the object language being written horizontally. The context $\Gamma$ is sometimes a series of typing judgements separated by commas $\Gamma=(a:A,b:B,c:C)$, but in a strengthened system we can have them be a type itself, $\Gamma=(a,b,c):A\times B\times C$. Turnstile denote derivability and $foo\vdash bar$ are classical sequents. Here I wonder if we really need to draw two dimensional and if not, then is the vertical axis the in-build meta-logic? When we write $\frac{A\ \ \ B}{C}$, the empty space between $A$ and $B$ must be a formalized "and". Curious then, that people were so motivated to work out the seemingly difficult task of giving semantics to product-types-lacking formal systems. Then people do untyped calculi in type theory, which is the same as collapsing one type. The logical propositions becomes the terms. Or we use the Curry Howard correspondence. Terms are proofs then, types are propositions. Hence function type $\to$ are implications $\implies$. When it comes to its categorical semantics, things get really out of hand. The first thing I read, in a depended type context, was that categories are the basic types and functors are implications in the logical interpretation. But then objects are the types and I figured these are objects with elements (like set) as types have terms. But the terms (or proofs, in the logical interpretation) are only contained in the objects in a sneaky way, because the objects are mostly the context. The morphisms are the turnstiles. But sometimes they are computer programs, i.e. proofs, i.e. the implications from a proposition (=type (=object)) to another. In fact, the are equivalence classes of computations w.r.t $\beta\eta$-conversion. But if you have 2-categories, then the 2-morphisms are the conversion. The last bit sounds reasonable to me. 
In any case, what is the most natural way to use type theory to capture propositional logic, so that I don't have to rewrite my notes completely once I pass to predicate logic? (=depended types (=fibered categories?)). My motivations are a clear presentation of math, not really proof theory and not a huge emphasis on computation.
 A: Since you are already familiar with the relevant concepts and approaches like fibered categories and the Curry-Howard isomorphism, I am not completely sure what exactly you are looking for. I think you are looking for a categorical framework for describing and relating many different types of logic, propositional, predicate and maybe even higher order, modal or dependently typed. The most general systematic approach to categorical logic I know is by Bart Jacobs primarily in his thesis & in his book. There are also surveys of his approach in some of his early (mainly pre 1995) papers. His framework is based primarily on (combinations of) fibrations and covers advanced systems like Calculus of Constructions & Martin-Lof theory. This approach is related to Barendregt's Generalised Type Systems (aka Cubism). Here is nice concise survey by Jacobs that relates his and Barendregt's approaches.
The main orgainizing principle in Jacobs framework is to arrange expresions of the languages into levels like terms, propositions, types and kinds and then look at what kinds of dependecies can exist between expressions from different levels. More specifically level $L_2$ depends on level $L_1$ (written $L_2 \succ L_1$) if you can derive sequents $\Gamma \vdash A:L_1$ and $\Gamma, x:A \vdash B[x]:L_2$. For example propositional logic and equivalently simply typed lambda calculus has only one level called $Type$ and no dependencies. Martin-Lof type theory also has only one level but with the reflexive dependency $Type \succ Type$. Higher order calculi generally have at least a second level usually called $Kind$ with $Type \succ Kind$ and the axiom $\vdash Type : Kind$. Given a sequent calculus presentation of a logic this framework lets you determine the levels and dependencies and lays out the broad structure of the categorical sematics based on these. It also shows how to model the semantics of sum product and exponent types within and across the levels.
