Just as we can systematically derive the fundamental ideas of category theory as generalized logic in the co/end calculus,
We can systematically derive the fundamental ideas of metalogic, in the co/descent calculus of bifibrant double categories.
Composition and transformation of h-profunctors form a tensor-hom adjunction, and currying gives formulae for right extensions and lifts.
| $[\mathcal{R\otimes S},\mathcal{T}]$ | = | $\mathsf{\Pi}\, \mathrm{A}: \mathbb{A}.\; \mathsf{\Pi}\, \mathrm{C}:\mathbb{C}.\; (\mathsf{\Sigma}\, \mathrm{B}:\mathbb{B}.\; \mathcal{R}(\mathrm{A,B})\times \mathcal{S}(\mathrm{B,C}))\to \mathcal{T}(\mathrm{A,C})$ |
|---|---|---|
| $[\mathcal{S},\mathcal{R\to T}]$ | = | $\mathsf{\Pi}\, \mathrm{B}:\mathbb{B}.\; \mathsf{\Pi}\, \mathrm{C}:\mathbb{C}.\; \mathcal{S}(\mathrm{B,C})\to (\mathsf{\Pi}\, \mathrm{A}:\mathbb{A}.\; \mathcal{R}(\mathrm{A,B})\to \mathcal{T}(\mathrm{A,C}))$ |
| $[\mathcal{R},\mathcal{T\leftarrow S}]$ | = | $\mathsf{\Pi}\, \mathrm{A}:\mathbb{A}.\; \mathsf{\Pi}\, \mathrm{B}:\mathbb{B}.\; \mathcal{R}(\mathrm{A,B})\to (\mathsf{\Pi}\, \mathrm{C}:\mathbb{C}.\; \mathcal{S}(\mathrm{B,C})\to \mathcal{T}(\mathrm{A,C}))$ |
$\mathsf{\Pi}$ is a descent object which iso-inserts + equifies the composition actions by each outer logic.
$\mathsf{\Sigma}$ is a codescent object which iso-coinserts + coequifies the composition actions by the inner logic.
H-weighted co/limits are representations of extensions and lifts.