Constructing the fuzz map #
In tangled type theory, a given model element has extensions at each level below it. We have a "preferred" extension, and must find a way to compute the other extensions from that information. In order to do this, we need to be able to convert arbitrary model elements into "junk" at other levels, which can then be clearly interpreted as a "non-preferred" extension.
The fuzz maps perform this task. They are parametrised by a pair of type indices, representing
the source type level and target type level. At each pair of levels, the fuzz map is an injection
from tangles to litters. An arbitrary litter can only be the image of a fuzz map defined at a
single pair of type levels.
Treating the output of a fuzz map as a typed near-litter, its pos is always greater than
the pos of the input to the function. This ensures a well-foundedness condition that we use
in many places later.
Main declarations #
ConNF.fuzz: Converts a tangle into a "junk" litter.
We construct the fuzz map by first defining the auxiliary function chooseWf.
Suppose we wish to construct a function f : α → β with the constraint that for each α,
there is a predefined set of "denied" β values that it cannot take. Under some restrictions
based on the cardinalities of the denied set, we can construct such a function. We can in addition
require that f be injective if α has a well-order, which we will assume here.
The fuzz map that we will construct indeed satisfies these conditions.
Noncomputably chooses an element of β \ s, given #s < #β.
Equations
- ConNF.someOfMkLt s h = Exists.choose ⋯
Instances For
Equations
- ConNF.chooseWfCore deny h x f = ConNF.someOfMkLt ({z : β | ∃ (y : α) (h : r y x), f y h = z} ∪ deny x) ⋯
Instances For
Constructs an injective function f such that f x ∉ deny x.
Equations
- ConNF.chooseWf deny h = ⋯.fix (ConNF.chooseWfCore deny h)
Instances For
We construct the fuzz maps by constructing a set of image values to deny, and then choosing
arbitrarily from the remaining set. This uses the chooseWf results.
The majority of this section is spent proving that the set of values to deny isn't "too large", such that we could run out of available values for the function.
The set of elements of ν that fuzz _ t cannot be.
Equations
Instances For
We're done with proving technical results, now we can define the fuzz maps.
The fuzz map for a particular pair of type indices.
In tangled type theory, a given model element has extensions at each level below it. We have a "preferred" extension, and must find a way to compute the other extensions from that information. In order to do this, we need to be able to convert arbitrary model elements into "junk" at other levels, which can then be clearly interpreted as a "non-preferred" extension.
The fuzz maps perform this task. They are parametrised by a pair of type indices, representing
the source type level and target type level. At each pair of levels, the fuzz map is an injection
from tangles to litters. An arbitrary litter can only be the image of a fuzz map defined at a
single pair of type levels.
Treating the output of a fuzz map as a typed near-litter, its pos is always greater than
the pos of the input to the function. This ensures a well-foundedness condition that we use
in many places later.
Equations
- ConNF.fuzz hβγ t = { ν := ConNF.chooseWf ConNF.fuzzDeny ⋯ t, β := β, γ := γ, β_ne_γ := hβγ }