Email Gateway (Aug 22 2022 at 17:47): Email Gateway (Aug 22 2022 at 17:47):From: Lawrence Paulson <lp15@cam.ac.uk>
Funnily enough, the first Isabelle logic was constructive type theory. It is still distributed as CTT. It’s based on the original (extensional) Martin-Löf type theory of 1979. I’m not sure how feasible it is to transform that into an implementation of HOTT.
--lcp
Email Gateway (Aug 22 2022 at 17:48):From: Joshua Chen <joshua.chen@uni-bonn.de>
I've been implementing a HoTT object logic for my Masters
thesis, the approach follows that of the HoTT book
somewhat (extensional Martin-Löf type theory with
cumulative Russell-style universes, and explicit dependent
eliminators for many types).
At the moment I'm implementing type universes in ML aiming
towards a formalization of univalence.
It's still very much a work in progress and unfit for
doing any serious work in HoTT, but if you're interested
the source is available at
https://github.com/jaycech3n/HoTT.
Best wishes,
Josh
Last updated: Apr 19 2024 at 16:20 UTC