Martin Escardo and Paulo Oliva, October 2021, with later additions.

We have various versions of argmin and argmax with different assumptions.


\begin{code}

{-# OPTIONS --safe --without-K #-}

module Games.ArgMinMax where

open import MLTT.Spartan hiding (_+_ ; J)

\end{code}

In this version of argmin and argmax we a assume a finite domain with
a finite type of outcomes.

\begin{code}

module ArgMinMax-Fin where

 open import Fin.Embeddings
 open import Fin.Order
 open import Fin.Topology
 open import Fin.Type
 open import MLTT.SpartanList
 open import Naturals.Order
 open import Notation.Order
 open import NotionsOfDecidability.Complemented

\end{code}

Every inhabited complemented subset of Fin n has a least and a
greatest element.

\begin{code}

 Fin-wf : {n : β„•} (A : Fin n β†’ 𝓀 Μ‡ ) (rβ‚€ : Fin n)
        β†’ is-complemented A
        β†’ A rβ‚€
        β†’ Ξ£ r κž‰ Fin n , A r Γ— ((s : Fin n) β†’ A s β†’ r ≀ s)
 Fin-wf {𝓀} {succ n} A 𝟎 d a = 𝟎 , a , Ξ» s a' β†’ ⟨⟩
 Fin-wf {𝓀} {succ n} A (suc rβ‚€) d a = Ξ³
  where
   IH : Ξ£ r κž‰ Fin n , A (suc r) Γ— ((s : Fin n) β†’ A (suc s) β†’ r ≀ s)
   IH = Fin-wf {𝓀} {n} (Ξ» x β†’ A (suc x)) rβ‚€ (Ξ» x β†’ d (suc x)) a

   r : Fin n
   r = pr₁ IH

   b : A (suc r)
   b = pr₁ (prβ‚‚ IH)

   c : (s : Fin n) β†’ A (suc s) β†’ r ≀ s
   c = prβ‚‚ (prβ‚‚ IH)

   l : Β¬ A 𝟎 β†’ (s : Fin (succ n)) β†’ A s β†’ suc r ≀ s
   l ν 𝟎 a       = 𝟘-elim (ν a)
   l Ξ½ (suc x) a = c x a

   Ξ³ : Ξ£ r κž‰ Fin (succ n) , A r Γ— ((s : Fin (succ n)) β†’ A s β†’ r ≀ s)
   γ = Cases (d 𝟎)
        (Ξ» aβ‚€ β†’ 𝟎 , aβ‚€ , Ξ» s a' β†’ ⟨⟩)
        (Ξ» (Ξ½ : Β¬ A 𝟎) β†’ suc r , b , l Ξ½)

 Fin-co-wf : {n : β„•} (A : Fin n β†’ 𝓀 Μ‡ ) (rβ‚€ : Fin n)
           β†’ is-complemented A
           β†’ A rβ‚€
           β†’ Ξ£ r κž‰ Fin n , A r Γ— ((s : Fin n) β†’ A s β†’ s ≀ r)
 Fin-co-wf {𝓀} {succ n} A 𝟎 d a = Ξ³
  where
   Ξ΄ : is-decidable (Ξ£ i κž‰ Fin n , A (suc i))
   δ = Fin-Compact (A ∘ suc) (d ∘ suc)

   Ξ“ = Ξ£ r κž‰ Fin (succ n) , A r Γ— ((s : Fin (succ n)) β†’ A s β†’ s ≀ r)

   Ξ³ : Ξ“
   Ξ³ = Cases Ξ΄ f g
    where
     f : Ξ£ i κž‰ Fin n , A (suc i) β†’ Ξ“
     f (i , b) = suc r' , a' , h
      where
       IH : Ξ£ r' κž‰ Fin n , A (suc r') Γ— ((s' : Fin n) β†’ A (suc s') β†’ s' ≀ r')
       IH = Fin-co-wf {𝓀} {n} (A ∘ suc) i (d ∘ suc) b

       r' : Fin n
       r' = pr₁ IH

       a' : A (suc r')
       a' = pr₁ (prβ‚‚ IH)

       Ο• : (s' : Fin n) β†’ A (suc s') β†’ s' ≀ r'
       Ο• = prβ‚‚ (prβ‚‚ IH)

       h : (s : Fin (succ n)) β†’ A s β†’ s ≀ suc r'
       h 𝟎       c = ⋆
       h (suc x) c = Ο• x c

     g : Β¬ (Ξ£ i κž‰ Fin n , A (suc i)) β†’ Ξ“
     g ν = 𝟎 , a , h
      where
       h : (s : Fin (succ n)) β†’ A s β†’ s ≀ 𝟎
       h (suc x) c = 𝟘-elim (ν (x , c))
       h 𝟎       c = ⋆

 Fin-co-wf {𝓀} {succ n} A (suc x) d a = suc (pr₁ IH) , pr₁ (prβ‚‚ IH) , h
  where
   IH : Ξ£ r κž‰ Fin n , A (suc r) Γ— ((s : Fin n) β†’ A (suc s) β†’ s ≀ r)
   IH = Fin-co-wf {𝓀} {n} (A ∘ suc) x  (d ∘ suc) a

   h : (s : Fin (succ n)) β†’ A s β†’ s ≀ suc (pr₁ IH)
   h 𝟎       b = ⋆
   h (suc x) b = prβ‚‚ (prβ‚‚ IH) x b

 Fin-argmin : {a r : β„•} (p : Fin (succ a) β†’ Fin r)
            β†’ Ξ£ x κž‰ Fin (succ a) , ((y : Fin (succ a)) β†’ p x ≀ p y)
 Fin-argmin {0} p = 𝟎 , α
  where
   Ξ± : (y : Fin 1) β†’ p 𝟎 ≀ p y
   Ξ± 𝟎 = ≀-refl ⟦ p 𝟎 ⟧
 Fin-argmin {succ a} p = Ξ³
  where
   IH : Ξ£ x κž‰ Fin (succ a) , ((y : Fin (succ a)) β†’ p (suc x) ≀ p (suc y))
   IH = Fin-argmin {a} (p ∘ suc)

   x = pr₁ IH
   Ο• = prβ‚‚ IH

   Ξ³ : Ξ£ x' κž‰ Fin (succ (succ a)) , ((y : Fin (succ (succ a))) β†’ p x' ≀ p y)
   Ξ³ = h (≀-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc x) ⟧)
    where
     h : is-decidable (p 𝟎 ≀ p (suc x)) β†’ type-of Ξ³
     h (inl l) = 𝟎 , α
      where
       Ξ± : (y : (Fin (succ (succ a)))) β†’ p 𝟎 ≀ p y
       Ξ± 𝟎       = ≀-refl ⟦ p 𝟎 ⟧
       Ξ± (suc y) = ≀-trans ⟦ p 𝟎 ⟧ ⟦ p (suc x) ⟧ ⟦ p (suc y) ⟧ l (Ο• y)
     h (inr Ξ½) = suc x , Ξ±
      where
       Ξ± : (y : (Fin (succ (succ a)))) β†’ p (suc x) ≀ p y
       α 𝟎       = not-less-bigger-or-equal ⟦ p (suc x) ⟧ ⟦ p 𝟎 ⟧
                    (contrapositive (<-coarser-than-≀ ⟦ p 𝟎 ⟧ ⟦ p (suc x) ⟧) Ξ½)
       Ξ± (suc y) = Ο• y

 argmin : {a r : β„•} β†’ (Fin (succ a) β†’ Fin r) β†’ Fin (succ a)
 argmin p = pr₁ (Fin-argmin p)

 argmin-correct : {a r : β„•} (p : Fin (succ a) β†’ Fin r)
                β†’ (y : Fin (succ a)) β†’ p (argmin p) ≀ p y
 argmin-correct p = prβ‚‚ (Fin-argmin p)

 Fin-argmax : {a r : β„•} (p : Fin (succ a) β†’ Fin r)
            β†’ Ξ£ x κž‰ Fin (succ a) , ((y : Fin (succ a)) β†’ p y ≀ p x)
 Fin-argmax {0} p = 𝟎 , α
  where
   Ξ± : (y : Fin 1) β†’ p y ≀ p 𝟎
   Ξ± 𝟎 = ≀-refl ⟦ p 𝟎 ⟧
 Fin-argmax {succ a} p = Ξ³
  where
   IH : Ξ£ x κž‰ Fin (succ a) , ((y : Fin (succ a)) β†’ p (suc y) ≀ p (suc x))
   IH = Fin-argmax {a} (p ∘ suc)

   x = pr₁ IH
   Ο• = prβ‚‚ IH

   Ξ³ : Ξ£ x' κž‰ Fin (succ (succ a)) , ((y : Fin (succ (succ a))) β†’ p y ≀ p x')
   Ξ³ = h (≀-decidable ⟦ p (suc x) ⟧ ⟦ p 𝟎 ⟧)
    where
     h : is-decidable (p (suc x) ≀ p 𝟎) β†’ type-of Ξ³
     h (inl l) = 𝟎 , α
      where
       Ξ± : (y : (Fin (succ (succ a)))) β†’ p y ≀ p 𝟎
       Ξ± 𝟎       = ≀-refl ⟦ p 𝟎 ⟧
       Ξ± (suc y) = ≀-trans ⟦ p (suc y) ⟧ ⟦ p (suc x) ⟧ ⟦ p 𝟎 ⟧ (Ο• y) l
     h (inr Ξ½) = suc x , Ξ±
      where
       Ξ± : (y : (Fin (succ (succ a)))) β†’ p y ≀ p (suc x)
       α 𝟎       = not-less-bigger-or-equal ⟦ p 𝟎 ⟧ ⟦ p (suc x) ⟧
                    (contrapositive (<-coarser-than-≀ ⟦ p (suc x) ⟧ ⟦ p 𝟎 ⟧) Ξ½)
       Ξ± (suc y) = Ο• y

\end{code}

We could define argmin and argmax independently of their
specification, and then prove their specification:

\begin{code}

 argmin' : {a r : β„•} β†’ (Fin (succ a) β†’ Fin r) β†’ Fin (succ a)
 argmin' {0}      p = 𝟎
 argmin' {succ a} p = Ξ³
  where
   m : Fin (succ a)
   m = argmin' {a} (p ∘ suc)

   Ξ³ : Fin (succ (succ a))
   Ξ³ = Cases (≀-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc m) ⟧)
        (Ξ» (l : p 𝟎 ≀ p (suc m)) β†’ 𝟎)
        (Ξ» otherwise β†’ suc m)

 argmax' : {a r : β„•} β†’ (Fin (succ a) β†’ Fin r) β†’ Fin (succ a)
 argmax' {0}      p = 𝟎
 argmax' {succ a} p = Ξ³
  where
   m : Fin (succ a)
   m = argmax' {a} (p ∘ suc)

   Ξ³ : Fin (succ (succ a))
   Ξ³ = Cases (≀-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc m) ⟧)
        (Ξ» (l : p 𝟎 ≀ p (suc m)) β†’ suc m)
        (Ξ» otherwise β†’ 𝟎)

\end{code}

TODO. Complete the following.

\begin{code}

 {-
 argmax'-correct : {a r : β„•} (p : Fin (succ a) β†’ Fin r)
                β†’ ((y : Fin (succ a)) β†’ p y ≀ p (argmax p))
 argmax'-correct {0}      p 𝟎 = ≀-refl ⟦ p 𝟎 ⟧
 argmax'-correct {succ a} p y = h y
  where
   m : Fin (succ a)
   m = argmax {a} (p ∘ suc)

   IH : (y : Fin (succ a)) β†’ p (suc y) ≀ p (suc m)
   IH = argmax-correct {a} (p ∘ suc)

   Ξ³ : Fin (succ (succ a))
   Ξ³ = Cases (≀-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc m) ⟧)
        (Ξ» (l : ⟦ p 𝟎 ⟧ ≀ ⟦ p (suc m) ⟧) β†’ suc m)
        (Ξ» otherwise β†’ 𝟎)

   Ξ³β‚€ : p 𝟎 ≀ p (suc m) β†’ Ξ³ ＝ suc m
   Ξ³β‚€ = {!!}

   γ₁ : Β¬ (p 𝟎 ≀ p (suc m)) β†’ Ξ³ ＝ 𝟎
   γ₁ = {!!}


   h : (y : Fin (succ (succ a))) β†’ p y ≀ p Ξ³
   h 𝟎 = l
    where
     l : p 𝟎 ≀ p Ξ³
     l = Cases (≀-decidable ⟦ p 𝟎 ⟧ ⟦ p (suc m) ⟧)
          (Ξ» (l : p 𝟎 ≀ p (suc m)) β†’ transport (Ξ» - β†’ p 𝟎 ≀ p -) ((Ξ³β‚€ l)⁻¹) l)
          (Ξ» otherwise β†’ {!!})
   h (suc x) = l
    where
     l : p (suc x) ≀ p Ξ³
     l = {!!}
 -}

\end{code}

This version of argmin and argmax assumes a compact domain and a
finite type of outcomes.

\begin{code}

module ArgMinMax-Compact-Fin where

 open import Fin.Order
 open import Fin.Topology
 open import Fin.Type
 open import Notation.Order
 open import NotionsOfDecidability.Complemented
 open import TypeTopology.CompactTypes

 open ArgMinMax-Fin

 compact-argmax : {X : 𝓀 Μ‡ } {n : β„•} (p : X β†’ Fin n)
                β†’ is-Compact X
                β†’ X
                β†’ Ξ£ x κž‰ X , ((y : X) β†’ p y ≀ p x)
 compact-argmax {𝓀} {X} {n} p ΞΊ xβ‚€ = II I
  where
   A : Fin n β†’ 𝓀 Μ‡
   A r = Ξ£ x κž‰ X , p x ＝ r

   aβ‚€ : A (p xβ‚€)
   aβ‚€ = xβ‚€ , refl

   Ξ΄ : is-complemented A
   Ξ΄ r = ΞΊ (Ξ» x β†’ p x ＝ r) (Ξ» x β†’ Fin-is-discrete (p x) r)

   I : Ξ£ r κž‰ Fin n , A r Γ— ((s : Fin n) β†’ A s β†’ s ≀ r)
   I = Fin-co-wf A (p xβ‚€) Ξ΄ aβ‚€

   II : type-of I β†’ Ξ£ x κž‰ X , ((y : X) β†’ p y ≀ p x)
   II (.(p y) , ((y , refl) , Ο•)) = y , (Ξ» y β†’ Ο• (p y) (y , refl))

 compact-argmin : {X : 𝓀 Μ‡ } {n : β„•} (p : X β†’ Fin n)
                β†’ is-Compact X
                β†’ X
                β†’ Ξ£ x κž‰ X , ((y : X) β†’ p x ≀ p y)
 compact-argmin {𝓀} {X} {n} p ΞΊ xβ‚€ = II I
  where
   A : Fin n β†’ 𝓀 Μ‡
   A r = Ξ£ x κž‰ X , p x ＝ r

   aβ‚€ : A (p xβ‚€)
   aβ‚€ = xβ‚€ , refl

   Ξ΄ : is-complemented A
   Ξ΄ r = ΞΊ (Ξ» x β†’ p x ＝ r) (Ξ» x β†’ Fin-is-discrete (p x) r)

   I : Ξ£ r κž‰ Fin n , A r Γ— ((s : Fin n) β†’ A s β†’ r ≀ s)
   I = Fin-wf A (p xβ‚€) Ξ΄ aβ‚€

   II : type-of I β†’ Ξ£ x κž‰ X , ((y : X) β†’ p x ≀ p y)
   II (.(p y) , ((y , refl) , Ο•)) = y , (Ξ» y β†’ Ο• (p y) (y , refl))


\end{code}

Added 11th September 2024. Simplified and more efficient version for
the boolean-valued case.

\begin{code}

module ArgMinMax-Fin-𝟚 where

 open import Fin.Type
 open import MLTT.Two-Properties
 open import Naturals.Addition

 Minβ‚‚ : (i : β„•) β†’ (Fin (i + 1) β†’ 𝟚) β†’ 𝟚
 Minβ‚‚ 0        p = p 𝟎
 Minβ‚‚ (succ i) p = min𝟚 (p 𝟎) (Minβ‚‚ i (p ∘ suc))

 Maxβ‚‚ : (i : β„•) β†’ (Fin (i + 1) β†’ 𝟚) β†’ 𝟚
 Maxβ‚‚ 0        p = p 𝟎
 Maxβ‚‚ (succ i) p = max𝟚 (p 𝟎) (Maxβ‚‚ i (p ∘ suc))

 argMinβ‚‚ : (i : β„•) β†’ (Fin (i + 1) β†’ 𝟚) β†’ Fin (i + 1)
 argMinβ‚‚ 0        p = 𝟎
 argMinβ‚‚ (succ i) p =
  𝟚-equality-cases
   (Ξ» (_ : p 𝟎 ＝ β‚€) β†’ 𝟎)
   (Ξ» (_ : p 𝟎 ＝ ₁) β†’ suc (argMinβ‚‚ i (p ∘ suc)))

 argMaxβ‚‚ : (i : β„•) β†’ (Fin (i + 1) β†’ 𝟚) β†’ Fin (i + 1)
 argMaxβ‚‚ 0        p = 𝟎
 argMaxβ‚‚ (succ i) p =
  𝟚-equality-cases
   (Ξ» (_ : p 𝟎 ＝ β‚€) β†’ suc (argMaxβ‚‚ i (p ∘ suc)))
   (Ξ» (_ : p 𝟎 ＝ ₁) β†’ 𝟎)

 argMinβ‚‚-is-selection-for-Minβ‚‚ : (i : β„•)
                                 (p : Fin (i + 1) β†’ 𝟚)
                               β†’ p (argMinβ‚‚ i p) ＝ Minβ‚‚ i p
 argMinβ‚‚-is-selection-for-Minβ‚‚ 0        p = refl
 argMinβ‚‚-is-selection-for-Minβ‚‚ (succ i) p =
  𝟚-equality-cases
   (Ξ» (e : p 𝟎 ＝ β‚€)
      β†’ p (argMinβ‚‚ (succ i) p)        ＝⟨ ap p (𝟚-equality-casesβ‚€ e) ⟩
        p 𝟎                          ＝⟨ e ⟩
        β‚€                            ＝⟨refl⟩
        min𝟚 β‚€ (Minβ‚‚ i (p ∘ suc))     ＝⟨ ap (Ξ» - β†’ min𝟚 - (Minβ‚‚ i (p ∘ suc))) (e ⁻¹) ⟩
        min𝟚 (p 𝟎) (Minβ‚‚ i (p ∘ suc)) ＝⟨refl⟩
        Minβ‚‚ (succ i) p               ∎)
   (Ξ» (e : p 𝟎 ＝ ₁)
     β†’ p (argMinβ‚‚ (succ i) p)        ＝⟨ ap p (𝟚-equality-cases₁ e) ⟩
       p (suc (argMinβ‚‚ i (p ∘ suc))) ＝⟨ argMinβ‚‚-is-selection-for-Minβ‚‚ i (p ∘ suc) ⟩
       Minβ‚‚ i (p ∘ suc)              ＝⟨refl⟩
       min𝟚 ₁ (Minβ‚‚ i (p ∘ suc))     ＝⟨ ap (Ξ» - β†’ min𝟚 - (Minβ‚‚ i (p ∘ suc))) (e ⁻¹) ⟩
       min𝟚 (p 𝟎) (Minβ‚‚ i (p ∘ suc)) ＝⟨refl⟩
       Minβ‚‚ (succ i) p               ∎)

 argMaxβ‚‚-is-selection-for-Maxβ‚‚ : (i : β„•)
                                 (p : Fin (i + 1) β†’ 𝟚)
                               β†’ p (argMaxβ‚‚ i p) ＝ Maxβ‚‚ i p
 argMaxβ‚‚-is-selection-for-Maxβ‚‚ 0        p = refl
 argMaxβ‚‚-is-selection-for-Maxβ‚‚ (succ i) p =
  𝟚-equality-cases
   (Ξ» (e : p 𝟎 ＝ β‚€)
     β†’ p (argMaxβ‚‚ (succ i) p)        ＝⟨ ap p (𝟚-equality-casesβ‚€ e) ⟩
       p (suc (argMaxβ‚‚ i (p ∘ suc))) ＝⟨ argMaxβ‚‚-is-selection-for-Maxβ‚‚ i (p ∘ suc) ⟩
       Maxβ‚‚ i (p ∘ suc)              ＝⟨refl⟩
       max𝟚 β‚€ (Maxβ‚‚ i (p ∘ suc))     ＝⟨ ap (Ξ» - β†’ max𝟚 - (Maxβ‚‚ i (p ∘ suc))) (e ⁻¹) ⟩
       max𝟚 (p 𝟎) (Maxβ‚‚ i (p ∘ suc)) ＝⟨refl⟩
       Maxβ‚‚ (succ i) p               ∎)
   (Ξ» (e : p 𝟎 ＝ ₁)
      β†’ p (argMaxβ‚‚ (succ i) p)        ＝⟨ ap p (𝟚-equality-cases₁ e) ⟩
        p 𝟎                          ＝⟨ e ⟩
        ₁                            ＝⟨refl⟩
        max𝟚 ₁ (Maxβ‚‚ i (p ∘ suc))     ＝⟨ ap (Ξ» - β†’ max𝟚 - (Maxβ‚‚ i (p ∘ suc))) (e ⁻¹) ⟩
        max𝟚 (p 𝟎) (Maxβ‚‚ i (p ∘ suc)) ＝⟨refl⟩
        Maxβ‚‚ (succ i) p               ∎)

\end{code}

Added 3rd March 2026. Moved and refined from the alpha-beta file.

This version of argmin and argmax assumes a listed domain and
any type of outcomes that has a decidable order.

\begin{code}

module ArgMinMax-Listed
        {𝓀 π“₯ : Universe}
        (R : 𝓀 Μ‡ )
        (_<_ : R β†’ R β†’ π“₯ Μ‡ )
        (Ξ΄ : (r s : R) β†’ is-decidable (r < s))
      where

 open import MLTT.List

 _β‰₯_ _≀_ : R β†’ R β†’ π“₯ Μ‡
 r β‰₯ s = Β¬ (r < s)
 s ≀ r = r β‰₯ s

 private
  min' max' : (r s : R) β†’ is-decidable (r < s) β†’ R

  min' r s (inl lt) = r
  min' r s (inr ge) = s

  max' r s (inl lt) = s
  max' r s (inr ge) = r

 min max : R β†’ R β†’ R
 min r s = min' r s (Ξ΄ r s)
 max r s = max' r s (Ξ΄ r s)

 open import MonadOnTypes.K
 open K-definitions R

 Min Max : {X : 𝓀 Μ‡ } β†’ listed⁺ X β†’ K X
 Min (xβ‚€ , xs , _) p = foldr (Ξ» x β†’ min (p x)) (p xβ‚€) xs
 Max (xβ‚€ , xs , _) p = foldr (Ξ» x β†’ max (p x)) (p xβ‚€) xs

 private
  argmin' argmax' : {X : 𝓀 Μ‡ } (p : X β†’ R) (x y : X) β†’ is-decidable (p x < p y) β†’ X

  argmin' p x y (inl le) = x
  argmin' p x y (inr ge) = y

  argmax' p x y (inl le) = y
  argmax' p x y (inr ge) = x

  argmin'-spec : {X : 𝓀 Μ‡ } (p : X β†’ R) (x y : X) (d : is-decidable (p x < p y))
               β†’ p (argmin' p x y d) ＝ min' (p x) (p y) d
  argmin'-spec p x y (inl lt) = refl
  argmin'-spec p x y (inr ge) = refl

  argmax'-spec : {X : 𝓀 Μ‡ } (p : X β†’ R) (x y : X) (d : is-decidable (p x < p y))
               β†’ p (argmax' p x y d) ＝ max' (p x) (p y) d
  argmax'-spec p x y (inl lt) = refl
  argmax'-spec p x y (inr ge) = refl


 argmin argmax : {X : 𝓀 Μ‡ } β†’ (X β†’ R) β†’ X β†’ X β†’ X

 argmin p x y = argmin' p x y (Ξ΄ (p x) (p y))
 argmax p x y = argmax' p x y (Ξ΄ (p x) (p y))


 argmin-spec : {X : 𝓀 Μ‡ } (p : X β†’ R) (x y : X)
             β†’ p (argmin p x y) ＝ min (p x) (p y)
 argmin-spec p x y = argmin'-spec p x y (Ξ΄ (p x) (p y))

 argmax-spec : {X : 𝓀 Μ‡ } (p : X β†’ R) (x y : X)
             β†’ p (argmax p x y) ＝ max (p x) (p y)
 argmax-spec p x y = argmax'-spec p x y (Ξ΄ (p x) (p y))

 open import MonadOnTypes.J
 open J-definitions R

 ArgMin ArgMax : {X : 𝓀 Μ‡ } β†’ listed⁺ X β†’ J X
 ArgMin (xβ‚€ , xs , _) p = foldr (argmin p) xβ‚€ xs
 ArgMax (xβ‚€ , xs , _) p = foldr (argmax p) xβ‚€ xs

 open import MonadOnTypes.JK R

 ArgMin-spec : {X : 𝓀 Μ‡ } (β„“ : listed⁺ X) β†’ (ArgMin β„“) attains (Min β„“)
 ArgMin-spec {X} (xβ‚€ , xs , m) p = I xs
  where
   I : (xs : List X)
     β†’ p (foldr (argmin p) xβ‚€ xs) ＝ foldr (Ξ» x β†’ min (p x)) (p xβ‚€) xs
   I [] = refl
   I (x ∷ xs) = Iβ‚€
    where
     IH : p (foldr (argmin p) xβ‚€ xs) ＝ foldr (Ξ» x β†’ min (p x)) (p xβ‚€) xs
     IH = I xs

     Iβ‚€ = p (argmin p x (foldr (argmin p) xβ‚€ xs))         ＝⟨ I₁ ⟩
          min (p x) (p (foldr (argmin p) xβ‚€ xs))          ＝⟨ Iβ‚‚ ⟩
          min (p x) (foldr (Ξ» x₁ β†’ min (p x₁)) (p xβ‚€) xs) ∎
           where
            I₁ = argmin-spec p x (foldr (argmin p) xβ‚€ xs)
            Iβ‚‚ = ap (min (p x)) IH

 ArgMax-spec : {X : 𝓀 Μ‡ } (β„“ : listed⁺ X) β†’ (ArgMax β„“) attains (Max β„“)
 ArgMax-spec {X} (xβ‚€ , xs , m) p = I xs
  where
   I : (xs : List X)
     β†’ p (foldr (argmax p) xβ‚€ xs) ＝ foldr (Ξ» x β†’ max (p x)) (p xβ‚€) xs
   I [] = refl
   I (x ∷ xs) = Iβ‚€
    where
     IH : p (foldr (argmax p) xβ‚€ xs) ＝ foldr (Ξ» x β†’ max (p x)) (p xβ‚€) xs
     IH = I xs

     Iβ‚€ = p (argmax p x (foldr (argmax p) xβ‚€ xs))         ＝⟨ I₁ ⟩
          max (p x) (p (foldr (argmax p) xβ‚€ xs))          ＝⟨ Iβ‚‚ ⟩
          max (p x) (foldr (Ξ» x₁ β†’ max (p x₁)) (p xβ‚€) xs) ∎
           where
            I₁ = argmax-spec p x (foldr (argmax p) xβ‚€ xs)
            Iβ‚‚ = ap (max (p x)) IH

\end{code}