hott injection

Stream: general

[Jakob von Raumer]

what is the hott-safe replacement for injection? Say I have e : sum.inl a = sum.inr b in the context and want to solve the goal by pointing out that contradiction...

[David Michael Roberts]

Presumably that the homotopy fibre is a subsingleton...

[Floris van Doorn]

The automatically generated no_confusion is not compatible with HoTT, and currently, there is no automatically-generated replacement. You have to prove yourself that sum.inl a = sum.inr b is impossible and that sum.inl and sum.inr are injective.

[Floris van Doorn]

It's done here for nat which works essentially in the same way: https://github.com/gebner/hott3/blob/master/src/hott/types/nat/basic.lean#L51-L71

[Floris van Doorn]

(succ_inj is proven a couple lines below that)

[Jakob von Raumer]

Okay, I started porting types/sum.hlean...

[Floris van Doorn]

Just so you know: there is more ported on my branch, https://github.com/fpvandoorn/hott3
I haven't ported sum yet. Also, it doesn't currently compile. If I have time I'll look at it tomorrow, and see if I can clean it up and push it to the main repo.