{-# 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₂