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...

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