Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] The Arithmetic Site in Isabelle/CTT (was: Isab...

Email Gateway (Aug 22 2022 at 18:08):

From: Lawrence Paulson <lp15@cam.ac.uk>
CTT is a fragment of Martin-Löf's Type Theory with extensional equality. See e.g.

http://www.cse.chalmers.se/research/group/logic/book/book.pdf <http://www.cse.chalmers.se/research/group/logic/book/book.pdf>

I can’t recall whether universes are covered, but maybe you don’t need them.

Larry

Last updated: Apr 25 2024 at 08:20 UTC