Daniel R. Grayson

intrusive notations

1

These notations ``` Module Export Notation. Notation ap := maponpaths. Notation "p # x" := (transportf _ p x) (right associativity, at level 65) : transport. Open Scope transport. Notation...

silly lemma

3

In light of ``` @isofhlevelff : ∏ (n : ℕ) (X Y Z : UU) (f : X → Y) (g : Y → Z), isofhlevelf n (λ x :...

... between ``` Definition unitset : hSet := hSetpair unit isasetunit. ``` and ``` Definition unitHSET : HSET. Proof. exists unit. abstract (apply isasetunit). Defined. ``` The second definition should...

comments contain things that creep into the TAGS file

1

``` /Users/dan/src/ProofChecking/UniMath/UniMath-exact-categories/UniMath/Algebra/Lattice.v 4: Definition of /Users/dan/src/ProofChecking/UniMath/UniMath-exact-categories/UniMath/CategoryTheory/limits/cones.v 3: Definition of /Users/dan/src/ProofChecking/UniMath/UniMath-exact-categories/UniMath/CategoryTheory/limits/pushouts.v 3: Definition of /Users/dan/src/ProofChecking/UniMath/UniMath-exact-categories/UniMath/CategoryTheory/limits/cats/limits.v 9: Definition of /Users/dan/src/ProofChecking/UniMath/UniMath-exact-categories/UniMath/CategoryTheory/limits/graphs/eqdiag.v 11: Example of /Users/dan/src/ProofChecking/UniMath/UniMath-exact-categories/UniMath/CategoryTheory/Inductives/Trees.v 3: Definition of /Users/dan/src/ProofChecking/UniMath/UniMath-exact-categories/UniMath/CategoryTheory/Bicategories/BicatAliases.v 4: Definition of /Users/dan/src/ProofChecking/UniMath/UniMath-exact-categories/UniMath/CategoryTheory/Monoidal/Strengths.v...

some definitions

9

These definitions should be changed so the equations are part of the property: ``` Definition isCokernel {x y z : C} (f : x --> y) (g : y -->...

*_rect

3

See the comment at https://github.com/UniMath/UniMath/pull/567#discussion_r101888918 Rename induction principles such as UU_rect to UU_rec, after #567 gets merged. Also think about making interfaces to them more uniform. Also add notations, such...

ambiguous coercions

4

I'm beginning to suspect that having multiple coercion paths between two classes is a bad idea, for making proofs easily. Does anyone else think so? Here is what's bugging me...

functions starting with "is" should have propositions as values

2

We should strive for predicates with suggestive names starting with "is" to be predicates in the sense that their values are propositions, for all valid arguments. Corresponding to that, the...

``` prod_precategory = λ C D : precategory, prod_precategory_data C D,, prod_precategory_is_precategory C D : precategory → precategory → precategory precategory_binproduct = λ C D : precategory, precategory_binproduct_data C D,,...

making propositions into hProps

1

Some definitions of ours are propositions but not declared as hProps. Is there any disadvantage to making them so? I have in mind, in particular, some things in category theory,...