# Maximum on the standard finite types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Amélia Liao.

Created on 2022-07-05.

module elementary-number-theory.maximum-standard-finite-types where

Imports
open import elementary-number-theory.inequality-standard-finite-types
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.unit-type

open import order-theory.least-upper-bounds-posets

open import univalent-combinatorics.standard-finite-types


## Idea

We define the operation of maximum (least upper bound) for the standard finite types.

## Definition

max-Fin : (k : ℕ) → Fin k → Fin k → Fin k
max-Fin (succ-ℕ k) (inl x) (inl y) = inl (max-Fin k x y)
max-Fin (succ-ℕ k) (inl x) (inr _) = inr star
max-Fin (succ-ℕ k) (inr _) (inl x) = inr star
max-Fin (succ-ℕ k) (inr _) (inr _) = inr star

max-Fin-Fin : (n k : ℕ) → (Fin (succ-ℕ n) → Fin k) → Fin k
max-Fin-Fin zero-ℕ k f =
f (inr star)
max-Fin-Fin (succ-ℕ n) k f =
max-Fin k (f (inr star)) (max-Fin-Fin n k (λ k → f (inl k)))


## Properties

### Maximum is greatest lower bound

leq-max-Fin :
(k : ℕ) (l m n : Fin k) →
leq-Fin k m l → leq-Fin k n l → leq-Fin k (max-Fin k m n) l
leq-max-Fin (succ-ℕ k) (inl x) (inl y) (inl z) p q = leq-max-Fin k x y z p q
leq-max-Fin (succ-ℕ k) (inr x) (inl y) (inl z) p q = star
leq-max-Fin (succ-ℕ k) (inr x) (inl y) (inr z) p q = star
leq-max-Fin (succ-ℕ k) (inr x) (inr y) (inl z) p q = star
leq-max-Fin (succ-ℕ k) (inr x) (inr y) (inr z) p q = star

leq-left-leq-max-Fin :
(k : ℕ) (l m n : Fin k) → leq-Fin k (max-Fin k m n) l → leq-Fin k m l
leq-left-leq-max-Fin (succ-ℕ k) (inl x) (inl y) (inl z) p =
leq-left-leq-max-Fin k x y z p
leq-left-leq-max-Fin (succ-ℕ k) (inr x) (inl y) (inl z) p = star
leq-left-leq-max-Fin (succ-ℕ k) (inr x) (inl y) (inr z) p = star
leq-left-leq-max-Fin (succ-ℕ k) (inr x) (inr y) (inl z) p = star
leq-left-leq-max-Fin (succ-ℕ k) (inr x) (inr y) (inr z) p = star
leq-left-leq-max-Fin (succ-ℕ k) (inl x) (inr y) (inr z) p = p

leq-right-leq-max-Fin :
(k : ℕ) (l m n : Fin k) → leq-Fin k (max-Fin k m n) l → leq-Fin k n l
leq-right-leq-max-Fin (succ-ℕ k) (inl x) (inl y) (inl z) p =
leq-right-leq-max-Fin k x y z p
leq-right-leq-max-Fin (succ-ℕ k) (inr x) (inl y) (inl z) p = star
leq-right-leq-max-Fin (succ-ℕ k) (inr x) (inl y) (inr z) p = star
leq-right-leq-max-Fin (succ-ℕ k) (inr x) (inr y) (inl z) p = star
leq-right-leq-max-Fin (succ-ℕ k) (inr x) (inr y) (inr z) p = star
leq-right-leq-max-Fin (succ-ℕ k) (inl x) (inl y) (inr z) p = p

is-least-upper-bound-max-Fin :
(k : ℕ) (m n : Fin k) →
is-least-binary-upper-bound-Poset (Fin-Poset k) m n (max-Fin k m n)
is-least-upper-bound-max-Fin k m n =
prove-is-least-binary-upper-bound-Poset
( Fin-Poset k)
( ( leq-left-leq-max-Fin k
( max-Fin k m n)
( m)
( n)
( refl-leq-Fin k (max-Fin k m n))) ,
( leq-right-leq-max-Fin k
( max-Fin k m n)
( m)
( n)
( refl-leq-Fin k (max-Fin k m n))))
( λ x (H , K) → leq-max-Fin k x m n H K)