Change implementation of Inductive Order on Nat (#1283)

* use boolean comparison in `Nat.Order.Inductive`, add non-strict and flipped inductive order, make faster instance search in `Fin.Literals`

* fix typo

Author: LorenzoMolena

Cubical/CW/Approximation.agda

@@ -380,8 +380,7 @@ finCWmap→CellMap n C D f =
     ... | inr n>m | inr n>sucm =
          cong (CW↪ D m)
            (funExt⁻ (cong (fmap ϕ) (ΣPathP (refl , (isProp<ᵗ _ _)))) x)
-       ∙ fcomm ϕ (m , <→<ᵗ n>m) x
-       ∙ funExt⁻ (cong (fmap ϕ) (ΣPathP (refl , (isProp<ᵗ _ _)))) _
+       ∙ fcomm ϕ (m , <ᵗ-trans (<→<ᵗ n>sucm) <ᵗsucm) x
 
     silly : (x : _) → smap ψ n x ≡ fmap ϕ (n , <ᵗsucm {n}) x
     silly x with (Dichotomyℕ n n)

Cubical/Data/Fin/Base.agda

@@ -65,6 +65,10 @@ fromℕ≤ : (m n : ℕ) → m ≤′ n → Fin (suc n)
 fromℕ≤ zero _ _ = fzero
 fromℕ≤ (suc m) (suc n) m≤n = fsuc (fromℕ≤ m n m≤n)
 
+-- Conversion from ℕ with an inductive definition of ≤
+fromℕ≤ᵗ : (m n : ℕ) → m ≤ᵗ n → Fin (suc n)
+fromℕ≤ᵗ m n t = m , t
+
 -- A case analysis helper for induction.
 fsplit
   : ∀(fj : Fin (suc k))

Cubical/Data/Fin/Literals.agda

@@ -6,13 +6,13 @@ open import Agda.Builtin.Nat
 open import Agda.Builtin.FromNat
   renaming (Number to HasFromNat)
 open import Cubical.Data.Fin.Base
-  using (Fin; fromℕ≤)
-open import Cubical.Data.Nat.Order.Recursive
-  using (_≤_)
+  using (Fin; fromℕ≤ᵗ)
+open import Cubical.Data.Nat.Order.Inductive
+  using (_≤ᵗ_)
 
 instance
   fromNatFin : {n : _} → HasFromNat (Fin (suc n))
   fromNatFin {n} = record
-    { Constraint = λ m → m ≤ n
-    ; fromNat    = λ m ⦃ m≤n ⦄ → fromℕ≤ m n m≤n
+    { Constraint = λ m → m ≤ᵗ n
+    ; fromNat    = λ m ⦃ m≤n ⦄ → fromℕ≤ᵗ m n m≤n
     }

Cubical/Data/Nat/Order/Inductive.agda

@@ -9,17 +9,44 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Unit
 open import Cubical.Data.Sigma
 
+open import Cubical.Data.Bool.Base hiding (_≟_)
+
 open import Cubical.Induction.WellFounded
 
 open import Cubical.Relation.Nullary
 
 -- TODO: unify with recursive.agda
 
--- inductive definition of <
+-- alternative definition of <
 _<ᵗ_ : (n m : ℕ) → Type
-n <ᵗ zero = ⊥
-zero <ᵗ suc m = Unit
-suc n <ᵗ suc m = n <ᵗ m
+n <ᵗ m = Bool→Type (n <ᵇ m)
+
+_≤ᵗ_ : (n m : ℕ) → Type
+n ≤ᵗ m = n <ᵗ suc m
+
+_>ᵗ_ : (n m : ℕ) → Type
+n >ᵗ m = m <ᵗ n
+
+_≥ᵗ_ : (n m : ℕ) → Type
+n ≥ᵗ m = m ≤ᵗ n
+
+-- <ᵗ satisfies the following judgmental equalities,
+-- which give <ᵗ an "inductive" presentation, justifying the module name:
+private
+  _ : ∀ {n} → n <ᵗ zero ≡ ⊥
+  _ = refl
+
+  _ : ∀ {m} → zero <ᵗ suc m ≡ Unit
+  _ = refl
+
+  _ : ∀ {n m} → suc n <ᵗ suc m ≡ n <ᵗ m
+  _ = refl
+
+  -- direct inductive definition (avoided for performance reasons):
+  -- _<ᵗ_ : (n m : ℕ) → Type
+  -- n <ᵗ zero = ⊥
+  -- zero <ᵗ suc m = Unit
+  -- suc n <ᵗ suc m = n <ᵗ m
 
 data Trichotomyᵗ (m n : ℕ) : Type₀ where
   lt : m <ᵗ n → Trichotomyᵗ m n