Redirected from "projection valued measure".
Contents
Idea
In dependent type theories with more than one layer of type, dependent extension types are types which behave like dependent product types except the index type is the outer layer of type rather than the normal layer of type. Thus, dependent extension types can be defined in simplicial type theory and cubical type theory.
Definition
In type theory with shapes
In type theory with shapes, there are three different layers - there are the cube layer and the tope layer, which is logic over type theory where the cubes are the types and the topes are the propositions in the logic over type theory, and finally there is the type layer, which is a dependent type theory.
Shapes are formed in the usual set-builder notation in set theory: given a cube and a predicate tope , one could construct the shape . A cofibration in a type theory with shapes is an inclusion of shapes, which means shapes and with a predicate .
Formation rules for dependent extension types:
Introduction rules for dependent extension types:
Elimination rules for dependent extension types
Computation rules for dependent extension types
Uniqueness rules for dependent extension types
In two-level type theory
In two-level type theory, there are two different layers of types - there is the pretype or non-fibrant layer and there is the type or fibrant layer. A cofibration in two-level type theory is an inclusion of pretypes, which means pretypes and and an embedding . The rules for dependent extension types are then given as follows:
Formation rules for dependent extension types
Introduction rules for dependent extension types
Elimination rules for dependent extension types
Computation rules for dependent extension types
Uniqueness rules for dependent extension types
Now, if the pretype layer has a Tarski type of all propositions , then given a pretype and predicates , , one could construct the shapes defined in the above section via the dependent sum type in the pretype layer:
The additional requirement above that implies that is a subtype of with an embedding in the pretype layer.
References