Bas Spitters

@mattam82 Indeed, as we say in the paper there are two proofs: one using a polymorphic Omega, the other using the mapping cone. The former one is formalized in Coq.

@mattam82 Indeed, there are two proofs. One using a polymorphic Omega, one using the mapping cone. The former is the one that I formalized.

After talking to @mattam82 yesterday, I think we now understand what is going on. The equivalence epis are surjective can be proved in regular categories. Regular categories are categories with...

Hi Hugo, Latest Ubuntu. Latest hoqc from git. Here is the output: Unable to parse accelerator 'MOD1i' for action 'Display implicit arguments' Unable to parse accelerator 'MOD1c' for action 'Display...

Hi Jesse, Thanks for the suggestion. I tried it, but the problem remains. COQBIN= COQLIB= COQTOP=/home/spitters/local/hoqc/coq/ I'd like to see the error message in the pop-up window, but it disappears...

Both have the same behavior. Incidentally, the makefile appears to be slightly non-standard. The COQTOP variable should be set to the path to the coqtop binary. Usually it is Coq's...

I have a separate coqide for 8.4 which works fine. hoqide from HoTT/HoTT and coqide from HoTT/coq both give these problems. > > Incidentally, the makefile appears to be slightly...

On Sun, Feb 3, 2013 at 3:14 PM, Bas Spitters [email protected] wrote: > > > Incidentally, the makefile appears to be slightly non-standard. > > > The COQTOP variable should...

Thanks! Where is it? I've looked for ExprImp in bedrock2, but it does not seem show the C backend.

@mattam82 Did you have the chance to look into this? It's also blocking some other programs we'd like to extract. Thanks!