Bas Spitters

The exists tactic works for records BTW. We are currently not using Canonical Structures/ Type Classes a lot, so the benefits are less clear. Our statements look less nice than...

> With the first projection of hProp declared as a coercion and the second > as an instance, the unbundled version is applicable wherever the bundled > one would be,...

@EgbertRijke will know more...

Is it related to this one? ``` Require Import HoTT. Require Import quotient. Definition Type2:=Type. Definition Type1:=Type:Type2. Variable A:Type1. Variable rel :A-> A-> Type2. Variable relset: setrel rel. Definition Quot:Type1:=...

The patch adds user syntax `Type@{(max U V)}`. We can then write: ``` Private Inductive quotient (sR:setrel R@{U V}): Type @{(max U V)} := | class_of : (A:Type@{U}) -> quotient...

As this is now part of: https://github.com/HoTT/HoTT/blob/master/STYLE.md#universes-and-hits shall we close this?

@mattam82 I am trying the quotient example above. I though the notation max was now allowed. However, it is missing from https://coq.inria.fr/refman/Reference-Manual032.html#sec784 Coq tells me: ``` Syntax error: [universe] expected...

I am inclined to say yes. On Tue, Feb 3, 2015 at 2:36 AM, Jason Gross [email protected] wrote: > Should we make more notations for equivalences, like + for >...

There is an Emacs plugin that does this for agda. I wonder how hard it is to port this to Coq. https://alhassy.github.io/next-700-module-systems/ A more principled approach would probably use meta-coq....

Here is the way type classes are implemented in lean. https://arxiv.org/abs/2001.04301 It's likely that this is useful for Coq too. One reason why we unbundle classes is to be able...