univalence and coercions

Stream: Type theory

[RustyYato]

Disclaimer: I'm aware that this topic doesn't strictly follow this stream's description since it's not specific to Lean, but I think this is the closest stream here.

I am studying univalence and univalent theorem provers on my own, and I have some questions about it. My biggest one, is as follows: is thinking of a univalent type theory as "a type theory where two terms are considered equal if there is an invertible coercion between them" correct (at least to an approximation)? If not, why? If so, are there any caveats?

Then the equality type is a subset of invertible coercions between terms of a given type. Which subset is type-dependent. Then propext and funext follow naturally, since they are pretty much stated in as of invertible coercions imply equality.

[François G. Dorais]

Note that Lean has no current plans to support univalence. You will certainly have better responses elsewhere.

You haven't quite understood equality in univalent type theory: equality is a type not a proposition. The type a = b can be quite complex and each element leads to a different "coercion" (better called "transport").

If equality is a Prop and propext is true, then univalence leads to a fairly quick contradiction.

[RustyYato]

I had thought so, but I was having a hard time finding the relevant forums, so I decided to ask here first. I've now found, https://agda.zulipchat.com/#narrow/channel/260790-cubical which seems promising. Thanks for your help!

[Trebor Huang]

Agda people seems to be more active on discord channels

[Bas Spitters]

hott.zulipchat.com/ would probably be the best place to ask such questions.

[RustyYato]

Oh, thanks everyone, that's very helpful!