I can help with syntactic things. The rest seems to be just intuitionistic logic.
This paper is referenced from the pfla book you are reading, in the chapter on equality. I thought, what's the hard bit that deserved a paper - Leibniz vs Martin-Löf equality looks trivial. But then proving their isomorphism is the tricky business.
no subject
Date: 2021-08-30 02:51 pm (UTC)So weird.
no subject
Date: 2021-08-31 09:42 am (UTC)no subject
Date: 2021-08-31 03:58 pm (UTC)Still weird; I'm trying to read it, but it seems like without having a decent knowledge of Agda, it's hardly possible to understand.
no subject
Date: 2021-08-31 05:12 pm (UTC)This paper is referenced from the pfla book you are reading, in the chapter on equality. I thought, what's the hard bit that deserved a paper - Leibniz vs Martin-Löf equality looks trivial. But then proving their isomorphism is the tricky business.
no subject
Date: 2021-10-02 05:54 pm (UTC)It basically amounts to a claim that Yo f a is isomorphic to f a, when f is a Functor:
data Yo f a = Yo {unYo :: ∀r . (a → r) → f r }Then for Functor Id we get ∀r . (a → r) → r is isomorphic to a.no subject
Date: 2021-10-02 08:50 pm (UTC)Right; later I figured that it's basically all about Yoneda.