Vladimir Voevodsky

A bit more work probably. In this case “famhomotfun” should not be in PartA because it requires the concept of homotopy for functions between types outside of UU and all...

It is nevertheless not good for PartA - the type of h involves the equalities in UU and they are not elements of UU. The types of arguments of functions/operations...

I am very doubtful about it. With this change, try “Print Universes” at the end of PartA and at the end of PartB. How many new universes have been generated...

This looks interesting! Can we remove the constraint? Adding extra constraints slows things down and in this case it is unnecessary. > On Mar 10, 2017, at 7:36 PM, Daniel...

Also, have you tried to do Print Universes to see how many universes Coq generates in PartA and PartB in different regimes? > On Mar 10, 2017, at 7:36 PM,...

> On Mar 11, 2017, at 8:35 AM, Daniel R. Grayson wrote: > > Definition hProp@{i j} : Type@{j} := total2@{j} isaprop@{i}. (* i < j *) What does it...

total2 takes two arguments - a type X:U_a and a function X -> U_b The result is in U_{max a b}. What is total2@j ? > On Mar 11, 2017,...

Given i Type@{i}, what is the connection between (total2@{i} P : Type@{j}) and (total2@{j} P : Type@{j}) ? Are they definitionally equal? > On Mar 11, 2017, at 8:50 AM,...

Which particular definitions are duplicated? > On Jul 1, 2016, at 12:54 PM, Daniel R. Grayson [email protected] wrote: > > In general, this sounds like a good principle, but I...

Then I suggest the following modified version of the rule: "Formalizing a result or a group of results one should use the existing definitions wherever they are available. For example,...