WellFounded: Well-founded relations are irreflexive.

agda · Sep 24, 2024 · c34fd77 · c34fd77
1 parent 53e400e
commit c34fd77
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/Cubical/Induction/WellFounded.agda b/Cubical/Induction/WellFounded.agda
@@ -3,6 +3,7 @@
 module Cubical.Induction.WellFounded where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Relation.Nullary
 
 module _ {ℓ ℓ'} {A : Type ℓ} (_<_ : A → A → Type ℓ') where
   WFRec : ∀{ℓ''} → (A → Type ℓ'') → A → Type _
@@ -45,3 +46,12 @@ module _ {ℓ ℓ'} {A : Type ℓ} {_<_ : A → A → Type ℓ'} where
 
       induction-compute : ∀ x → induction x ≡ (e x λ y _ → induction y)
       induction-compute x = wfi-compute x (wf x)
+
+  wf→x≮x : WellFounded _<_ → ∀ {x} → ¬ (x < x)
+  wf→x≮x wf {x} = aux x (wf x)
+    where
+      aux : ∀ x → Acc _<_ x → ¬ (x < x)
+      aux x (acc r) x<x = aux x (r x x<x) x<x
+
+  wf→x<y→x≢y : WellFounded _<_ → ∀ {x} {y} → x < y → ¬ (x ≡ y)
+  wf→x<y→x≢y wf {x} x<y x≡y = wf→x≮x wf (subst (x <_) (sym x≡y) x<y)