The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hi Yannick,

That sounds great. Out of curiosity, what kind of barriers do you run into? And is it compatible with CoqHoTT? (I might need univalence for some of the theorems I'm interested in proving.)

The most immediate thing I want to do is determine show there is an equivalence (or show the necessary additional proof obligations with which there would be an equivalence) between the notion of a half-adjoint equivalence in HoTT, and a sort of deconstructed equivalence I use in my tool. But the deconstructed equivalence is defined in a way that sometimes depends on the constructors and eliminators of inductive types. This example includes one such deconstructed equivalence, plus a proof that it induces an actual equivalence. I'd like to show something like that more generally, but I can't even state the type of the deconstructed equivalence inside of Coq in general, since I need access to the types of constructors and eliminators for arbitrary inductive types.

Talia

On Tue, Oct 13, 2020 at 2:39 PM Yannick Forster <yannick AT yforster.de> wrote:

Hi Talia, 

MetaCoq embeds all of Coq in Coq. Given that your tool is really a tool concerned with Coq (right?), MetaCoq might be a good fit. One of the initial motivations of the project was exactly to enable the verification of plugins. 

If you give more context about the kind of theorem you want to prove about your tool I can try to help more how feasible it is to express that in MetaCoq. 

Best 

Yannick 

On 13 October 2020 23:33:01 Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi again!

I'd like to try out a proof about one of my tools, but to do so I need to introspect on the behavior of inductive constructors and eliminators, so I guess I need an embedding of CIC. It's OK for the purpose of this proof to use univalence, since my tool's metatheory is univalent. Is there an embedding of CIC I can play with, maybe in CoqHoTT?

Talia