Vincent Semeria

@Zimmi48 Because CoRN `Require Import` Coq's standard library, CoRN is forced to be LGPL. Or am I missing something ?

@Zimmi48 Who is interpreting the license now ? You say that LGPL is complicated so we should avoid it, but eventually CoRN imports files from the standard library. If there...

> I agree that what you propose is very simple. @Zimmi48 Great, let's keep it simple. This is complicated enough already. > If some day, Coq's standard library itself is...

@Zimmi48 The option to use a later version of the license is already given in each file ``` * This work is free software; you can redistribute it and/or modify...

@Zimmi48 Is it good now with meta.yml modified and the templates regenerated ?

@Zimmi48 I regenerated the templates and `.travis.yml` is back. It still does not build though. `opam install coq-corn.dev -v -y -j 2' failed`.

@Zimmi48 Now branch master builds, but not the previous branches `make: *** No rule to make target 'install'. Stop.`

What do you call the type of finite sets ? Is it something like ``` Fixpoint Fin (n : nat) : Set := match n with | O => Empty_set...

As you said "the 0-truncation definition makes them behave much more like most mathematicians expect cardinal numbers to behave". When they are not trained in HoTT and its language, most...

Also, your position that a set is not its cardinal is inconsistent with the definition 10.3.17 of ordinals. 10.3.17 defines an ordinal as a well-order. But likewise, ZFC says that...