It's tempting to think that one can define univalence without universes,
but I don't think this rule makes sense:

On Sat, Oct 8, 2022 at 6:59 AM Madeleine Birchfield <
madeleinebirchfield@gmail.com> wrote:

> The elimination rule says that given a judgment 'A type' in context Gamma,
> a judgment 'B type' in context Gamma, a judgment 'C(p) type' in the context
> 'Gamma, p : A = B', and a judgment 't:C(refl_A)' in the context 'Gamma',
> one could form the conclusion 'J(t, p): C(p)' in the context 'Gamma'


In the ordinary Id-elimination rule, the motive C has to be defined in the
context of two *variable* elements of the type and an equality between
them, not two *specific* elements.  In particular, if A and B are specific
types, then it doesn't make sense to substitute refl_A for p in C, because
you can't substitute A for B.  You can only substitute for a variable.

I think in order to do something like this, you have to augment type theory
by some kind of "polymorphism" that will allow you to hypothesize a "type
variable" in the context.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpwW0jL-EER%2BK3t7qs4_RegaB0CkZz6seMpRBw2SHGsr-Q%40mail.gmail.com.