Adding UIP-compatible univalence?

Stream: Type theory

[lyphyser]

The problem of adding traditional univalence to Lean would be that it is incompatible with UIP because there can be two distinct equivalence on pairs of types, which means two distinct equalities (e.g. id and flip in Bool).

But it seems this difficulty can be avoided by adopting a restricted form of univalence that only allows to get an equality from an equivalence for a single equivalence per type pair, and such that the set of those equivalences is closed under composition and type formation congruence, so that there is still only one equality per type pair.

Obviously the simplest way to realize this is to require a proof that the equivalence is unique.

It seems it might also be possible to make this work by having types come with globally selected ordering, requiring that the equivalence is minimal in the lexicographic ordering induced by it (probably needs both directions to be minimal) and perhaps some other requirements to ensure composition and type formation works.

Thoughts?

[lyphyser]

Another way could be to allow to specify an equivalence at type creation (with a new global directive similar to "instance") and check that the graph of those and those induced by applying type formers to them is acyclic and has no self loops (so that composition and type formation don't introduce two potentially different equalities for any pair of types or introduce an equality different than refl between a type and itself).

[Jannis Limperg]

This seems plausible, but is it useful? To me, the big benefit of univalence is "isomorphism induces equivalence". If that principle holds, then the two distinct isomorphisms of booleans need to induce two distinct equalities.

[lyphyser]

It would be restricted to "the unique 'canonical' isomorphism (if there is one) induces equality" with 'canonical' being defined using one of the criteria listed above (or something better if found).

[lyphyser]

Seems like allowing to choose an equivalence explictly is better than the requiring it to be minimal over an ordering, because you still need to effectively decide the ordering at type creation type, and specifying the equivalence directly seems much simpler than specifying an order.

It seems this mechanism would be powerful enough for instance to define binary naturals, provide the equivalence to make them be equal to the unary naturals, and define an instance of CommSemiring on them and prove that it is equal to the CommSemiring instance on N, and thus that any statement on commutative semirings that holds for unary naturals holds for binary naturals, and similarly any computation would give the same result (or more precisely the results would be HEq given HEq inputs)

[Trebor Huang]

Having a random equality doesn't really help. We need to be able to characterize what transporting along the equality does. So it would be next to useless to have that equality between binary and unary naturals unless we can prove that the additions and multiplications agree when you transport across the equality. That requires the full statement of univalence to prove in HoTT.

[lyphyser]

the equality would come from an equivalence, which consists of a function, an inverse function and two proofs that fun . invFun = id and invFun . fun = id; hence, transport can be performed by applying the function

[lyphyser]

it would like univalence, except the univalence axiom would have additional prerequisites that make sure that only one equality can be created between any two types

[Jannis Limperg]

LL said:

It seems this mechanism would be powerful enough for instance to define binary naturals, provide the equivalence to make them be equal to the unary naturals, and define an instance of CommSemiring on them and prove that it is equal to the CommSemiring instance on N, and thus that any statement on commutative semirings that holds for unary naturals holds for binary naturals, and similarly any computation would give the same result (or more precisely the results would be HEq given HEq inputs)

This works (I think) because we only operate on concrete types. But as soon as we abstract, we get into trouble. For instance, we'd like to prove that any two isomorphic CommSemirings are equal. However, this is not provable in your system because it only holds if the underlying isomorphism of types is the canonical one. In order to prove a general result, you'd have to introduce the special predicate "f is the canonical isomorphism between α and β". But even this result is much weaker than what you'd get in full HoTT.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

One thing to note is that in Lean, UIP follows from definitional proof irrelevance and the fact that Eq is a Prop. You can simply define a Type-valued identity type with no definitional UIP. This is what GroundZero does.

[Kyle Miller]

@Wojciech Nawrocki You also need to avoid subsingleton elimination though, right? The hott example a few lines down successfully fails (I think I heard that hott is checking for subsingleton elimination), but in plain Lean UIP would go through just fine.

Here's Type-valued UIP in plain Lean to save a click:

universe u

inductive TEq {α : Type u} : α -> α -> Type u where
  | refl (x : α) : TEq x x

def TEq.uip {α : Type u} {x y : α} (p q : TEq x y) : TEq p q := by
  cases p; cases q; apply refl

[Kyle Miller]

(I don't really know what I'm talking about here, so I might be using the wrong terminology, sorry!)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Absolutely, I forgot about that feature!

[Kyle Miller]

I'm a bit confused, since subsingleton elimination doesn't apply to TEq as it's not a Prop.

However, looking at the term for TEq.uip, it turns out cases silently uses UIP, pulling in Eq.ndrec to rewrite indices. That should be enough to trigger the hott check at least, and that's where subsingleton elimination is being used.

[Robert Maxton]

Jannis Limperg said:

@_LL|751429 said:

It seems this mechanism would be powerful enough for instance to define binary naturals, provide the equivalence to make them be equal to the unary naturals, and define an instance of CommSemiring on them and prove that it is equal to the CommSemiring instance on N, and thus that any statement on commutative semirings that holds for unary naturals holds for binary naturals, and similarly any computation would give the same result (or more precisely the results would be HEq given HEq inputs)

This works (I think) because we only operate on concrete types. But as soon as we abstract, we get into trouble. For instance, we'd like to prove that any two isomorphic CommSemirings are equal. However, this is not provable in your system because it only holds if the underlying isomorphism of types is the canonical one. In order to prove a general result, you'd have to introduce the special predicate "f is the canonical isomorphism between α and β". But even this result is much weaker than what you'd get in full HoTT.

Wouldn't this essentially be the same as providing some syntactic sugar for inductive types that are immediately quotiented by a given relation? So handling the "canonical isomorphism" would be handled by the existing Quot/Quotient API.