fix defintions of min and max, add comment on limitations of UsingEq (#1270)

Author: LorenzoMolena

Cubical/Data/Nat/Properties.agda

@@ -23,9 +23,9 @@ private
 min : ℕ → ℕ → ℕ
 min zero m = zero
 min (suc n) zero = zero
-min (suc n) (suc m) with n <ᵇ m
-... | false = suc m
-... | true  = suc n
+min (suc n) (suc m) with n <ᵇ m UsingEq
+... | false , _ = suc m
+... | true  , _ = suc n
 
 minSuc : min (suc n) (suc m) ≡ suc (min n m)
 minSuc {zero} {zero} = refl
@@ -44,9 +44,9 @@ minComm (suc n) (suc m) = minSuc ∙∙ cong suc (minComm n m) ∙∙ sym minSuc
 max : ℕ → ℕ → ℕ
 max zero m = m
 max (suc n) zero = suc n
-max (suc n) (suc m) with n <ᵇ m
-... | false = suc n
-... | true  = suc m
+max (suc n) (suc m) with n <ᵇ m UsingEq
+... | false , _ = suc n
+... | true  , _ = suc m
 
 maxSuc : max (suc n) (suc m) ≡ suc (max n m)
 maxSuc {zero} {zero} = refl

Cubical/Foundations/Prelude.agda

@@ -506,6 +506,9 @@ infixl 0 _i0:>_UsingEqP
 
 -- Similar to `inspect`, but more convenient when `a` is not a function
 -- application, or when the applied function is not relevant
+-- Note: when defining a term with `UsingEq`, it's still possible to prove its properties
+-- using a with-abstraction without `UsingEq`, but not the other way around.
+-- See `min`/`max` and their properties in Data.Nat.Properties for examples of this.
 _UsingEq : (a : A) → singl a
 a UsingEq = isContrSingl a .fst