Conversation

Any two terms in a STLC with unit, products and functions (and no base types) are equal. I didn't find a quick reference for this, so I wrote a proof here: github.com/nachivpn/coher Comments welcome!

github.com

GitHub - nachivpn/coherence: Proof of coherence for the initial CCC

Proof of coherence for the initial CCC. Contribute to nachivpn/coherence development by creating an account on GitHub.

Replying to

and

I just want to say this Agda looks really nice! I like the fact that you lean a bit on words - I find Agda code that leans in the other direction quite impenetrable!

11:22 AM · Mar 11, 2019Twitter Web Client

Replying to

Thanks :D