local-set-theory

Musings on local set theory based on the book

• John Bell. Toposes and local set theories: An introduction. 1988.

File descriptions:

• coq/deep_embedding.v : deep embedding, that is a model of the syntax in Coq
• coq/shallow_embedding.v : shallow embedding, that is an embedding into the logic of Coq
• elpi/theory.elpi : a tiny proof assistant in ELPI (lambda prolog)
• elpi/theorems.elpi : theorems and their proofs in local set theory