port 2Sphere1 and Pi1S2 from Dan Licata's Agda Library about coq-hott

[mdnahas]

I'm giving up on this to focus on the Coq code for the first half of the book.

[andrejbauer]

Huh, how are you doing this? We should first have that Python script. Let me see what I can do.

[mdnahas]

I was doing it by hand. A script can transliterate the Agda, but we wanted
a proof that used the HoTT Coq Library.

I was mostly doing it so that I could learn the HoTT Coq Library. But it
required also learning Dan's library and understanding the differences
between the two (and some more HoTT theory) to translate the proof.

I ran into enough trouble that I felt I should concentrate on The Book
first and then come back to Pi?S?s if they were still undone.

Mike

On Fri, Mar 15, 2013 at 1:16 PM, Andrej Bauer [email protected]:

Huh, how are you doing this? We should first have that Python script. Let
me see what I can do.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/92#issuecomment-14973385
.

[awodey]

I believe Andrej is talking about coqing the Book, not Dan's Agda proof.

S

I was doing it by hand. A script can transliterate the Agda, but we
wanted
a proof that used the HoTT Coq Library.

I was mostly doing it so that I could learn the HoTT Coq Library. But it
required also learning Dan's library and understanding the differences
between the two (and some more HoTT theory) to translate the proof.

I ran into enough trouble that I felt I should concentrate on The Book
first and then come back to Pi?S?s if they were still undone.

Mike

On Fri, Mar 15, 2013 at 1:16 PM, Andrej Bauer
[email protected]:

Huh, how are you doing this? We should first have that Python script.
Let
me see what I can do.

—
Reply to this email directly or view it on
GitHubhttps://github.com//issues/92#issuecomment-14973385
.

---

Reply to this email directly or view it on GitHub:
#92 (comment)

[andrejbauer]

Yes, sorry, I was confused.

[andrejbauer]

This is obsolete.