Profile cover photo
Profile photo
Marc de Falco
45 followers
45 followers
About
Posts

Post has attachment
Chapter 2 in the Agda proof assistant
I've decided this morning to learn a bit of Agda. Here's what I've done today, it goes through chapter 2 proving everything in Agda by staying as close to possible to the book (for example when multiple proof terms worked, I've chosen the same one). I've al...
Chapter 2 in the Agda proof assistant
Chapter 2 in the Agda proof assistant
steppingintohott.blogspot.com
Add a comment...

Post has attachment
2.3 -- An explanation of "Type families as fibrations" using diagrams (Part 1)
I'm often in need of diagrams for understanding abstract concepts. I perfectly understand why there's not a lot of diagram in HOTT book : it was made in a very short time to explain the theory in the doing. Here I'll try to re-explain 2.3 using diagrams. I ...
Add a comment...

Post has attachment
2.7 -- Functoriality of ap under $\sum$-types
(I won't start with the introductory issues of HOTT, as it very well explained. Instead, I'll present what was lately on my scratchpad. ) The statement of this lemma and its proof was left to the reader and it gave me some trouble to state it right. First, ...
Add a comment...
Wait while more posts are being loaded