module A202401.DBI {π} {X : Set π} where
open import A202401.Prelude public
infix 3 _β_
data _β_ : Rist X β X β Set π where
zero : β {Ξ A} β Ξ , A β A
wkβ : β {B Ξ A} (i : Ξ β A) β Ξ , B β A
injwkβ : β {Ξ A B} {i iβ² : Ξ β A} β wkβ i β‘ wkβ {B} iβ² β i β‘ iβ²
injwkβ refl = refl
infix 4 _ββ_
_ββ_ : β {Ξ A} (i iβ² : Ξ β A) β Dec (i β‘ iβ²)
zero ββ zero = yes refl
zero ββ wkβ iβ² = no Ξ» ()
wkβ i ββ zero = no Ξ» ()
wkβ i ββ wkβ iβ² with i ββ iβ²
... | yes refl = yes refl
... | no Β¬eq = no Ξ» { refl β refl β― Β¬eq }