Zulip Chat Archive
Stream: Type theory
Topic: externalization
Reid Barton (May 13 2020 at 19:41):
Mario Carneiro said:
I think the most powerful form of this would be a proof translator that takes proofs in e.g. cubicaltt and reflects them into a model of cubical type theory in lean
A more classical version of this is to take a proof in e.g. Lean (that doesn't use the wrong axioms) and turn it into a statement about a topos.
Reid Barton (May 13 2020 at 19:41):
Maybe @Bhavik Mehta would like to do this? :upside_down:
Reid Barton (May 13 2020 at 19:41):
I think it's really hard.
Bhavik Mehta (May 13 2020 at 19:41):
I wouuuuld
Bhavik Mehta (May 13 2020 at 19:42):
But I probably shouldn't disappear into that rabbit hole any time soon
Reid Barton (May 13 2020 at 19:42):
Also I think there might be some similar work in progress in Coq, let me see if I can find any information about this
Reid Barton (May 13 2020 at 19:44):
Hopefully this will make more sense to you than it does to me: https://github.com/CoqHott/coq-forcing
Reid Barton (May 13 2020 at 19:44):
Oh, you're already on the hott zulip.
Reid Barton (May 13 2020 at 19:44):
Bhavik Mehta (Aug 27 2020 at 20:46):
By the way, I got to the end of Power world in NNG but in terms of a natural numbers object internal to a cartesian closed category
Last updated: Dec 20 2023 at 11:08 UTC