[ add ] wellfoundedness of Relation.Binary.Construct.Add.Infimum.Strict

CHANGELOG.md

@@ -197,6 +197,13 @@ Additions to existing modules
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
 
+* In `Relation.Binary.Construct.Add.Infimum.Strict`:
+  ```agda
+  <₋-accessible-⊥₋ : Acc _<₋_ ⊥₋
+  <₋-accessible[_] : Acc _<_ x → Acc _<₋_ [ x ]
+  <₋-wellFounded   : WellFounded _<_ → WellFounded _<₋_
+  ```
+
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec : Dec {a} ⊤

src/Relation/Binary/Construct/Add/Infimum/Strict.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The lifting of a non-strict order to incorporate a new infimum
+-- The lifting of a strict order to incorporate a new infimum
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -17,6 +17,7 @@ module Relation.Binary.Construct.Add.Infimum.Strict
 open import Level using (_⊔_)
 open import Data.Product.Base using (_,_; map)
 open import Function.Base using (_∘_)
+open import Induction.WellFounded using (WfRec; Acc; acc; WellFounded)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; cong; subst)
 import Relation.Binary.PropositionalEquality.Properties as ≡
@@ -35,6 +36,7 @@ open import Relation.Nullary.Construct.Add.Infimum
   using (⊥₋; [_]; _₋; ≡-dec; []-injective)
 import Relation.Nullary.Decidable.Core as Dec using (map′)
 
+
 ------------------------------------------------------------------------
 -- Definition
 
@@ -72,14 +74,28 @@ module _ {r} {_≤_ : Rel A r} where
   open NonStrict _≤_
 
   <₋-transʳ : Trans _≤_ _<_ _<_ → Trans _≤₋_ _<₋_ _<₋_
-  <₋-transʳ <-transʳ (⊥₋≤ .⊥₋) (⊥₋<[ l ]) = ⊥₋<[ l ]
-  <₋-transʳ <-transʳ (⊥₋≤ l)   [ q ]  = ⊥₋<[ _ ]
-  <₋-transʳ <-transʳ [ p ]     [ q ]  = [ <-transʳ p q ]
+  <₋-transʳ <-transʳ (⊥₋≤ ⊥₋)  q   = q
+  <₋-transʳ <-transʳ (⊥₋≤ _) [ q ] = ⊥₋<[ _ ]
+  <₋-transʳ <-transʳ [ p ]   [ q ] = [ <-transʳ p q ]
 
   <₋-transˡ : Trans _<_ _≤_ _<_ → Trans _<₋_ _≤₋_ _<₋_
-  <₋-transˡ <-transˡ ⊥₋<[ l ] [ q ] = ⊥₋<[ _ ]
+  <₋-transˡ <-transˡ ⊥₋<[ _ ] [ q ] = ⊥₋<[ _ ]
   <₋-transˡ <-transˡ [ p ]    [ q ] = [ <-transˡ p q ]
 
+<₋-accessible-⊥₋ : Acc _<₋_ ⊥₋
+<₋-accessible-⊥₋ = acc λ()
+
+<₋-accessible[_] : ∀ {x} → Acc _<_ x → Acc _<₋_ [ x ]
+<₋-accessible[_] = acc ∘ wf-acc
+  where
+  wf-acc : ∀ {x} → Acc _<_ x → WfRec _<₋_ (Acc _<₋_) [ x ]
+  wf-acc _       ⊥₋<[ _ ] = <₋-accessible-⊥₋
+  wf-acc (acc ih) [ y<x ] = <₋-accessible[ ih y<x ]
+
+<₋-wellFounded : WellFounded _<_ → WellFounded _<₋_
+<₋-wellFounded wf ⊥₋    = <₋-accessible-⊥₋
+<₋-wellFounded wf [ x ] = <₋-accessible[ wf x ]
+
 ------------------------------------------------------------------------
 -- Relational properties + propositional equality