Need fixity

[Sofia-Insa]

Those functions need a fixity.

• Relation.Binary.Construct.Add.Extrema.NonStrict

_≤⊤± : ∀ k → k ≤± ⊤±
⊥±    ≤⊤± = ⊥±≤⊤±
[ k ] ≤⊤± = [ k ]≤⊤±
⊤±    ≤⊤± = ⊤±≤⊤± 

This function establishes that the minimal element ⊥± is less than or equal to all elements k.

_≤⊤± : ∀ k → k ≤± ⊤±
⊥±    ≤⊤± = ⊥±≤⊤±
[ k ] ≤⊤± = [ k ]≤⊤±
⊤±    ≤⊤± = ⊤±≤⊤±

This function establishes that all elements k is less than or equal to the maximal element.
those functions were added agda/agda-stdlib@3cefa71

• Relation.Binary.Construct.Add.Infimum.NonStrict

-- Definition
infix 5 _≤₋_
data _≤₋_ : Rel (A ₋) (a ⊔ ℓ) where
  ⊥₋≤_  : (l : A ₋)         → ⊥₋    ≤₋ l
  [_] : {k l : A} → k ≤ l → [ k ] ≤₋ [ l ]

⊥₋≤_ is a constructor

• Data.Container.Indexed.Combinator

_^⊥ : Container I O c r → Container I O (c ⊔ r) c
(C ^⊥) .Command  o     = (c : C .Command o) → C .Response c
(C ^⊥) .Response {o} _ = C .Command o
(C ^⊥) .next     f c   = C .next c (f c)

agda/agda-stdlib@747351e

• Effect.Monad.Partiality

data _⊥ (A : Set a) : Set a where
  now   : (x : A) → A ⊥
  later : (x : ∞ (A ⊥)) → A ⊥

data _⊥P : Set a → Set (Level.suc a) where
  now   : (x : A) → A ⊥P
  later : (x : ∞ (A ⊥P)) → A ⊥P
  _>>=_ : (x : A ⊥P) (f : A → B ⊥P) → B ⊥P

data _⊥ added agda/agda-stdlib@5c22331

agda/agda-stdlib@3aaaab9 data _⊥-whnf added to the file infixl 1 _>>=_
agda/agda-stdlib@c15d12c data _⊥-whnf changed to data _⊥P