{-# OPTIONS --type-in-type #-}

open import Base
open import Equality

module Properties where

-- Synonyms ------------------------------------------

Not : Set → Set
Not A = A → False

Rel : Set → Set
Rel A = A → A → Set

Equiv : (A : Set) → Rel A
Equiv A = _≡_ {_} {A}

-- Properties ----------------------------------------

Reflexive : {A : Set} → Rel A → Set
Reflexive {A} _~_ = {a : A} → a ~ a

Irreflexive : {A : Set} → Rel A → Set
Irreflexive {A} _~_ = {a : A} → Not (a ~ a)

Symmetric : {A : Set} → Rel A → Set
Symmetric {A} _~_ = {a b : A} → a ~ b → b ~ a

Asymmetric : {A : Set} → Rel A → Set
Asymmetric {A} _~_ = {a b : A} → a ~ b → Not (b ~ a)

Antisymmetric : {A : Set} → Rel A → Set
Antisymmetric {A} _~_ = {a b : A} → a ~ b → b ~ a → a ≡ b

Trans : {A : Set} → Rel A → Rel A → Rel A → Set
Trans {A} P Q R = {a b c : A} → P a b → Q b c → R a c

Trans2 : {A : Set} → Rel A → Rel A → Rel A → Rel A → Set
Trans2 {A} P Q R S = {a b c d : A} → P a b → Q b c → R c d → S a d

Trans3 : {A : Set} → Rel A → Rel A → Rel A → Rel A → Rel A → Set
Trans3 {A} P Q R S T = {a b c d e : A} → P a b → Q b c → R c d → S d e → T a e

Trans4 : {A : Set} → Rel A → Rel A → Rel A → Rel A → Rel A → Rel A → Set
Trans4 {A} P Q R S T U = {a b c d e f : A} → P a b → Q b c → R c d → S d e → T e f → U a f

Transitive : {A : Set} → Rel A → Set
Transitive R = Trans R R R

Transitive2 : {A : Set} → Rel A → Set
Transitive2 R = Trans2 R R R R

Transitive3 : {A : Set} → Rel A → Set
Transitive3 R = Trans3 R R R R R

Transitive4 : {A : Set} → Rel A → Set
Transitive4 R = Trans4 R R R R R R

Total : {A : Set} → Rel A → Set
Total {A} _~_ = {a b : A} → (a ~ b) ⊎ (b ~ a)

Trichotomy : (A B C : Set) → Set
Trichotomy A B C = (A × Not B × Not C) ⊎
                   (Not A × B × Not C) ⊎
                   (Not A × Not B × C)

Trichotomous : {A : Set} → Rel A → Set
Trichotomous {A} _~_ = {a b : A} → Trichotomy (a ≡ b) (a ~ b) (b ~ a)

Equivalence : {A : Set} → Rel A → Set
Equivalence R = Reflexive R × Symmetric R × Transitive R

Initial : {A : Set} → A → Rel A → Set
Initial {A} a₀ _~_  = {a : A} → a₀ ~ a

Final : {A : Set} → A → Rel A → Set
Final {A} a₀ _~_  = {a : A} → a ~ a₀

------------------------------------------------------

Associative : {A : Set} → Op A → Set
Associative {A} _⊕_ = {a b c : A} → (a ⊕ b) ⊕ c ≡ a ⊕ (b ⊕ c)

AssociativeR : {A : Set} → Op A → Set
AssociativeR {A} _⊕_ = {a b c : A} → a ⊕ (b ⊕ c) ≡ (a ⊕ b) ⊕ c

Comm : {A B : Set} → (A → A → B) → Set
Comm {A} _⊕_ = {a b : A} → a ⊕ b ≡ b ⊕ a

Commutative : {A : Set} → Op A → Set
Commutative = Comm

Idempotent : {A : Set} → Op A → Set
Idempotent {A} _⊕_ = {a : A} → a ⊕ a ≡ a

UnitL : {A : Set} → A → Op A → Set
UnitL {A} u _⊕_ = {a : A} → u ⊕ a ≡ a

UnitR : {A : Set} → A → Op A → Set
UnitR {A} u _⊕_ = {a : A} → a ⊕ u ≡ a

ZeroL : {A : Set} → A → Op A → Set
ZeroL {A} z _⊕_ = {a : A} → z ⊕ a ≡ z

ZeroR : {A : Set} → A → Op A → Set
ZeroR {A} z _⊕_ = {a : A} → a ⊕ z ≡ z

InverseL : {A : Set} → (A → A) → A → Op A → Set
InverseL {A} inverse u _⊕_ = {a : A} → inverse a ⊕ a ≡ u

InverseR : {A : Set} → (A → A) → A → Op A → Set
InverseR {A} inverse u _⊕_ = {a : A} → a ⊕ inverse a ≡ u

DistributiveL : {A : Set} → Op A → Op A → Set
DistributiveL {A} _⊗_ _⊕_ = {a b c : A} → a ⊗ (b ⊕ c) ≡ (a ⊗ b) ⊕ (a ⊗ c)

DistributiveR : {A : Set} → Op A → Op A → Set
DistributiveR {A} _⊗_ _⊕_ = {a b c : A} → (a ⊕ b) ⊗ c ≡ (a ⊗ c) ⊕ (b ⊗ c)


------------------------------------------------------

-- I should really create a more general case that subsumes both Injection and Injective

Injection : {A : Set} → Rel A → (A → A) → Set
Injection {A} _~_ f = {a b : A} → f a ~ f b → a ~ b

Injection2 : {A : Set} → Rel A → (A → A → A) → Set
Injection2 {A} _~_ f = {a₁ a₂ b₁ b₂ : A} → f a₁ b₁ ~ f a₂ b₂ → (a₁ ~ a₂) × (b₁ ~ b₂)

Injective : {A B : Set} → (A → B) → Set
Injective {A} f = {a b : A} → f a ≡ f b → a ≡ b

Injective2 : {A B C : Set} → (A → B → C) → Set
Injective2 {A} {B} f = {a₁ a₂ : A} → {b₁ b₂ : B} → f a₁ b₁ ≡ f a₂ b₂ → a₁ ≡ a₂ × b₁ ≡ b₂

CancellativeL : {A B C : Set} → (A → B → C) → Set
CancellativeL {A} f = {a : A} → Injective (f a)

CancellativeR : {A B C : Set} → (A → B → C) → Set
CancellativeR {A} {B} f = {a₁ a₂ : A} → {b : B} → f a₁ b ≡ f a₂ b → a₁ ≡ a₂

Congruent : {A B : Set} → (A → B) → Set
Congruent {A} f = {a b : A} → a ≡ b → f a ≡ f b

Congruent2 : {A B C : Set} → (A → B → C) → Set
Congruent2 {A} {B} f = {a₁ a₂ : A} → {b₁ b₂ : B} → a₁ ≡ a₂ → b₁ ≡ b₂ → f a₁ b₁ ≡ f a₂ b₂

Congruent2L : {A B C : Set} → (A → B → C) → Set
Congruent2L {A} {B} f = {a : A} → {b₁ b₂ : B} → b₁ ≡ b₂ → f a b₁ ≡ f a b₂

Congruent2R : {A B C : Set} → (A → B → C) → Set
Congruent2R {A} {B} f = {a₁ a₂ : A} → {b : B} → a₁ ≡ a₂ → f a₁ b ≡ f a₂ b

Congruent3 : {A B C D : Set} → (A → B → C → D) → Set
Congruent3 {A} {B} {C} f = {a₁ a₂ : A} → {b₁ b₂ : B} → {c₁ c₂ : C} → a₁ ≡ a₂ → b₁ ≡ b₂ → c₁ ≡ c₂ → f a₁ b₁ c₁ ≡ f a₂ b₂ c₂

Congruent4 : {A B C D E : Set} → (A → B → C → D → E) → Set
Congruent4 {A} {B} {C} {D} f = {a₁ a₂ : A} → {b₁ b₂ : B} → {c₁ c₂ : C} → {d₁ d₂ : D} → a₁ ≡ a₂ → b₁ ≡ b₂ → c₁ ≡ c₂ → d₁ ≡ d₂ → f a₁ b₁ c₁ d₁ ≡ f a₂ b₂ c₂ d₂