Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
dependent_type_theory [2014/11/16 16:15] nikolaj |
dependent_type_theory [2014/11/16 16:15] nikolaj |
||
|---|---|---|---|
| Line 54: | Line 54: | ||
| Lastly, let's note that if one allows for rule schemas, then one really only needs dependent products and inductive types (and a universe of types). | Lastly, let's note that if one allows for rule schemas, then one really only needs dependent products and inductive types (and a universe of types). | ||
| - | == Characterization for $\Pi,\Sigma$ as adjoints == | + | == Characterization of $\Pi,\Sigma$ as adjoints == |
| The above construction "$\frac{input}{output}$" is in fact the object map of a functor and the introduction is right adjoint to the (pullback of the!) "weakening" of context, where one simply keeps track of an additional term: | The above construction "$\frac{input}{output}$" is in fact the object map of a functor and the introduction is right adjoint to the (pullback of the!) "weakening" of context, where one simply keeps track of an additional term: | ||
