Zulip Chat Archive

Stream: general

Topic: hott injection

Jakob von Raumer (Oct 22 2018 at 21:58):

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 (Oct 22 2018 at 22:44):

Presumably that the homotopy fibre is a subsingleton...

Floris van Doorn (Oct 22 2018 at 23:16):

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 (Oct 22 2018 at 23:16):

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 (Oct 22 2018 at 23:17):

(succ_inj is proven a couple lines below that)

Jakob von Raumer (Oct 22 2018 at 23:48):

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

Floris van Doorn (Oct 23 2018 at 03:48):

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.

Last updated: Aug 03 2023 at 10:10 UTC