Zulip Chat Archive

Stream: Type theory

Topic: externalization


view this post on Zulip 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.

view this post on Zulip Reid Barton (May 13 2020 at 19:41):

Maybe @Bhavik Mehta would like to do this? :upside_down:

view this post on Zulip Reid Barton (May 13 2020 at 19:41):

I think it's really hard.

view this post on Zulip Bhavik Mehta (May 13 2020 at 19:41):

I wouuuuld

view this post on Zulip Bhavik Mehta (May 13 2020 at 19:42):

But I probably shouldn't disappear into that rabbit hole any time soon

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 13 2020 at 19:44):

Oh, you're already on the hott zulip.

view this post on Zulip Reid Barton (May 13 2020 at 19:44):

https://hott.zulipchat.com/#narrow/stream/228519-general/topic/constructive.20lemmas.20in.20practice/near/192758167

view this post on Zulip 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: May 08 2021 at 22:13 UTC