coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] the homotopical fiber of the predecessor function

From: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
To: coq-club AT inria.fr
Cc: univalent-mathematics AT googlegroups.com
Subject: [Coq-Club] the homotopical fiber of the predecessor function
Date: Thu, 17 May 2018 12:03:59 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=josephcmac AT gmail.com; spf=Pass smtp.mailfrom=josephcmac AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f173.google.com
Ironport-phdr: 9a23:oDXoxhQgG6h+oYerAdcqb9FC49psv+yvbD5Q0YIujvd0So/mwa69bBaN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6ka4UPCPEBOvxAoIf6vVQOqwa+CheoBOz31jFIgWL53bc70+QuDAHJwg0hEMoQvXvOt9r6LqMSUeSrw6nSyjXIcvRb2TX66IjTbB8hufGMUq51ccXL1UYiDAzFjlCKpozkOzOZzPgCs2+e7+d5U++klmApqwZ0oje1x8csjJHEhoMPxVDf7yl23ps6JcC+RUVmYtCkCINduz+GO4ZyWM8vQGFltDwkxrEYt5O3ZjUGxZYpyhPZdveJaZKH4gj5W+aUOTp4hGxqeLa4hxuq9Eiv0Oz8Vs2t3FZLqSpJjsDAtn4Q2xHR5MWLUPR9/kCm2TaA0wDc9PtILlwzlareM5Ihw7gwmYQPsUnbACP6hEH7gLWVe0gk4OSk9frrb7v8qpOBNYJ5hBnyMqE0lcy+BeQ4PBIOX2+e+emk1r3j+lb5T6tSjv02jqbZtYrVKtgAq662Bg9ayIcj6xKlAzi619QYmGELLEhZdxKfk4jpJ1bOLejkAve4mlSgiStkx/TbPrL6GZjNNXjCkLL5fbln8UJcyQwzzcpe551OEL0BLujzCQfNs4nTCQZ8OAipyc7mDs9838UQQzGhGKicZYHVqt6/w+spPuSIU7UStCz8JOUo9cnFhHUwnVsQZ67hiZkQc32gHv9jKk6xbn/lg9NHGmAP6FltBNf2gUGPBGYAL025WLgxs2liWdCWSLzbT4Xou4SvmSKyH5lYfGdDUwneHnLhdoHCUPAJOnvLfp1R1wccXL3kcLcPkAm0vVajmbViJ+vQvCYfsMC7jYUn16jojRg3sAdMIYGd3mWKFT8mm2oJQ3o32/g6rxUikRGM1q93h/EeHttWtatE

Hello,

As a nice exercice, I was programming in Coq the contractibility of the homotopical fiber of the predecessor function (see below). I already proved that the fiber is nonempty, but there are some technical details at the end of the proof of contractibility, maybe involving transport. I'm just a self-taught beginner in Coq. My only theoretical reference for UniMath are Voevodsky's 6 lectures at Oxford in 2015 (the 3 first lectures were not filmed, so, I only have access to 3 last lectures): https://www.math.ias.edu/vladimir/Lectures

1) Could someone recommend me some tutorials in order to learn UniMath?

2) Is HoTT "better" than UniMath? In which sense?

Finally, any suggestion in order to finish my program below is welcome.

Thanks you in advance,

José M.

Require Import UniMath.Foundations.NaturalNumbers.

Require Import UniMath.Foundations.PartA.

Lemma hpredExistence (n : nat) (islarger0 : 0 < n) : hfiber S n.

Proof.

unfold hfiber.

induction n.

assert (K := negnatlthplusnmm 0 0).

rewrite natplusr0 in K.

contradiction.

intros.

induction (natchoice0 n).

rewrite <- a.

exists 0.

apply idpath.

apply IHn in b.

destruct b as [x H].

exists (S x).

apply (maponpaths S H).

Defined.

Theorem hpredExistenceUniqueness (n : nat) (islarger0 : 0 < n) : iscontr (hfiber S n).

Proof.

intros.

unfold iscontr.

exists (hpredExistence n islarger0).

intros.

set (s := hpredExistence n islarger0).

unfold hfiber in t.

unfold hfiber in s.

destruct t as [x H].

destruct s as [y K].

assert (J := K).

rewrite <- H in J.

assert ( JJ := pathsinv0 J ).

clear J.

apply invmaponpathsS in JJ as J.

[Coq-Club] the homotopical fiber of the predecessor function, José Manuel Rodriguez Caballero, 05/17/2018
- Re: [Coq-Club] the homotopical fiber of the predecessor function, Ralph Matthes, 05/17/2018