Expand description
Certified universe-polymorphic quotient primitives.
Observational equality: Obs.{u} A a b : SProp, an equality over every type that computes on
the weak-head normal form of A, with Obs_refl, Obs_transp (its elimination, into SProp only)
and Obs_cast (a value carried along an equality of types), after Pujet and Tabareau’s CC^obs.
register installs them beside the standard library, with the SProp connectives the rules
produce (STrue, SFalse, SAnd, SSigma, SBox and their projections) and EqvGen, the
equivalence closure of a relation, and certifies them: the kernels’ computation rules fire only
for the constants the certificate names, and displacing any name it rests on revokes it, as the
standard quotient’s certificate is.
Obs.{u} A a b, by the weak-head normal form of A:
A | a ~ b is |
|---|---|
Π (x : D). C | Π (x : D). a x ~[C] b x |
SProp | SAnd (a → b) (b → a) |
Prop | SAnd (SBox (a → b)) (SBox (b → a)) |
another universe, a and b types that are not propositions | by their formers: two universes equal when their levels are, two function types SSigma (D' ~ D) (λ e. Π (x' : D'). C[Obs_cast D' D e x'] ~ C'[x']), one inductive family or quotient former the conjunction of its arguments’ equalities, two different formers SFalse |
an inductive family that is not a proposition, a and b constructors | SFalse for two constructors, else the conjunction of the fields’ equalities |
a quotient that is not a proposition, a and b classes | SBox (EqvGen A r x y) of their representatives |
A conjunction is STrue for none and right-nested SAnd otherwise; a position whose type mentions
an earlier position compares heterogeneously, SSigma (T ~ T') (λ e. Obs_cast T T' e x ~ y), which
positions are dependent read off the telescope. Three guards keep the rules sound, each locked by
a test that derives SFalse without it: two proofs are never compared by their constructors (they
are one by irrelevance); a proposition seen as a type is never compared by its former (Nat → False and Bool → False are one proposition); and a family’s arguments are compared only when
its universe can store them (Hur: an injective I : (Type → Type) → Type refutes excluded
middle). Everything else is stuck.
Obs_cast.{u} A B e t computes where A ~ B does: along one universe to t; along two function
types to λ (x' : D'). Obs_cast C[back] C'[x'] (SSigma_snd … e x') (t back) with back the argument
carried back along the domains’ equality; along one family without indices whose parameters and
fields depend on no earlier one to the same constructor at the target parameters, each field
carried along an equality of its types built by Obs_transp; along one quotient former to the class
of the carried representative. A cast between propositions, along evidence of SFalse, along a
stuck type or of a value that is not yet a constructor is stuck.
Functions§
- register
- The
SPropconnectives and the four constants, certified.