module Basics where

{-
This file acts as a library of all the basic definitions used by other
files.
-}


open import Agda.Primitive

-------------------------------------------------------------------------
--equality relation
------------------------------------------------------------------------

data _≡_ {a : Level}{A : Set a}(x : A) : A → Set a  where
 refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

-----------------------------------------------------------------------
--dependent sum type
----------------------------------------------------------------------

record Σ {a b}(A : Set a)(B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public


Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
Σ-syntax = Σ

syntax Σ-syntax  A (λ x → B) = Σ[ x ∈ A ] B

--------------------------------------------------------------------
--product of two types
--------------------------------------------------------------------

_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ[ x ∈ A ] B

------------------------------------------------------------------
--the empty type
------------------------------------------------------------------

data ⊥ : Set  where


-----------------------------------------------------------------
--the unit type
----------------------------------------------------------------

record ⊤ : Set where
  constructor One


------------------------------------------------------------------
--boolean type
------------------------------------------------------------------

data 𝔹 : Set where
 true : 𝔹
 false : 𝔹

-----------------------------------------------------------------
--natural number type
-----------------------------------------------------------------

data ℕ : Set where
 zero : ℕ
 succ : ℕ → ℕ

-------------------------------------------------------------
--list type
-------------------------------------------------------------

data List (A : Set) : Set where
 [] : List A
 _::_ : A → List A → List A

------------------------------------------------------------
--vector type
-----------------------------------------------------------

data Vec (A : Set) : ℕ → Set where
 [] : Vec A zero
 _::_ : ∀ {n} → (a : A) → (as : Vec A n) → Vec A (succ n)


------------------------------------------------------------------
--disjoint sum
-----------------------------------------------------------------

data _⊎_ {ℓ₁ ℓ₂ : Level}(A : Set ℓ₁)(B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  inl : (x : A) → A ⊎ B
  inr : (y : B) → A ⊎ B

----------------------------------------------------------------
--decidable equality
---------------------------------------------------------------

data Dec {ℓ : Level} (X : Set ℓ) : Set ℓ where
  yes : X → Dec X
  no : (X → ⊥) → Dec X


----------------------------------------------------------------------------------------------
                                   --RELATIONS
----------------------------------------------------------------------------------------------

-------------------------------------------------------------------------------------------
--Definition
-------------------------------------------------------------------------------------------

Rel : (A : Set) → Set₁
Rel A = A → A → Set

------------------------------------------------------------------------------------------
--Reflexive, Symmetric and Transitive
------------------------------------------------------------------------------------------

Reflexive : (A : Set) → Rel A → Set
Reflexive A _≈_ = ∀ {i} → i ≈ i


Symmetric : (A : Set) → Rel A → Set
Symmetric A _≈_ = ∀ {i j} → i ≈ j → j ≈ i


Transitive : (A : Set) → Rel A → Set
Transitive A _≈_ = ∀ {i j k} → i ≈ j → j ≈ k → i ≈ k


record isEquivalence (A : Set)(_≈_ : Rel A) : Set where
  field
    Reflex : Reflexive A _≈_
    Symm : Symmetric A _≈_
    Trans : Transitive A _≈_

open isEquivalence public

-------------------------------------------------------------------------------------------
--_≡_ is an equivalence relation
-------------------------------------------------------------------------------------------

reflex : {A : Set} → (a : A) → a ≡ a
reflex a = refl


sym : {ℓ : Level}{A : Set ℓ} → {a b : A} → a ≡ b → b ≡ a
sym refl = refl


_≡<_>_ : {ℓ : Level} {A : Set ℓ} → (a : A) → { b c : A} → a ≡ b → b ≡ c → a ≡ c
a ≡< refl > refl = refl


aEquiv≡ : (A : Set) → isEquivalence A _≡_
aEquiv≡ A = record { Reflex = λ {p} → refl
                              ; Symm = λ {p q} → (λ p≡q → sym p≡q)
                              ; Trans = λ {p q r} → (λ p≡q → (λ q≡r → (p ≡< p≡q > q≡r)))
                              }

record Setoid : Set₁ where
  constructor ST
  field
     Carrier : Set 
     ≈ₛ     :  Rel Carrier 
     Eqv : isEquivalence Carrier ≈ₛ

open Setoid public

----------------------------------------------------------------------------------------------
--Preserving relations
---------------------------------------------------------------------------------------------

_Preserves_⟶_ : {A B : Set} → (f : A → B) → (_≈_ : Rel A) → (_≈_ : Rel B) → Set
f Preserves _≈ₚ_ ⟶ _≈ᵣ_ = ∀ {a₁ a₂} → a₁ ≈ₚ a₂ → (f a₁) ≈ᵣ (f a₂) 


_Preserves₂_⟶_⟶_ :{A B C : Set} → (f : A → B → C) → (_≈_ : Rel A) → (_≈_ : Rel B) → (_≈_ : Rel C) → Set
_++_ Preserves₂ _≈ₚ_ ⟶ _≈ᵣ_ ⟶ _≈ₛ_ = ∀ {a₁ a₂ b₁ b₂} →  a₁ ≈ₚ a₂ → b₁ ≈ᵣ b₂ → (_≈ₛ_) ( a₁ ++ b₁) ( a₂ ++ b₂)
 

------------------------------------------------------------------------------------------------
--Layout for equational reasoning for any equivalence relation
------------------------------------------------------------------------------------------------

_▪ : {ℓ : Level}{A : Set ℓ} → (x : A) → x ≡ x
x ▪ = refl

_≣<_and_by_as_on_>_ : {A : Set} → (a b c : A) → (_≈_ : Rel A) → (eq≈ : isEquivalence A _≈_) → a ≈ b → b ≈ c → a ≈ c
a ≣< b and c by _≈_ as eq≈ on a≈b > b≈c = (Trans eq≈) a≈b b≈c    


_by_as_▴ : {A : Set} → (x : A) → (_≈_ : Rel A) → (eq≈ : isEquivalence A _≈_) → x ≈ x
x by _≈_ as eq≈ ▴ = (Reflex eq≈) {x}

------------------------------------------------------------------------------------------
--equal things are related under any equivalence relation
------------------------------------------------------------------------------------------

≈≡ : {A : Set}{_≈_ : Rel A} → (eq : isEquivalence A _≈_) → {a₁ a₂ : A} → a₁ ≡ a₂ → a₁ ≈ a₂
≈≡ {A}{_≈_} eq {a₁} {.a₁} refl = (Reflex eq) {a₁} 


----------------------------------------------------------------------------------------------------------------------------------
                                                                --FUNCTIONS
----------------------------------------------------------------------------------------------------------------------------------


Op₁ : (A : Set) → Set
Op₁ A =  A → A


Op₂ : (A : Set) → Set
Op₂ A = A → A → A


_∘_ : {A B C : Set} → (g : B → C) → (f : A → B) → (A → C)
g ∘ f = λ x → g (f x)


cong : {ℓ₁ ℓ₂ : Level}{A : Set ℓ₁}{B : Set ℓ₂} → {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
cong f refl = refl 


congf : {ℓ : Level}{A B : Set ℓ} {f g : A → B} → f ≡ g → (x : A) → f x ≡ g x
congf refl x = refl


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


------------------------------------------------------------------------------------------------------------------------------
                                                --Group and Group Action axioms
------------------------------------------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------------------------
--associativity
------------------------------------------------------------------------------------------------------------

assoc : {A : Set}{_∙_ : Op₂ A}{_≈_ : Rel A} → Set
assoc {A} {_∙_}{_≈_} = ∀ x y z → (x ∙ (y ∙ z)) ≈ ((x ∙  y)∙ z)

----------------------------------------------------------------------------------------------------------
--identity
----------------------------------------------------------------------------------------------------------

idax : {A : Set}{_∙_ : Op₂ A}{_⁻¹ : Op₁ A}{_≈_ : Rel A} → A → Set
idax {A}{_∙_}{_⁻¹}{_≈_} e = ∀ x → (((( x ⁻¹ ) ∙ x) ≈ e ) × ((x ∙ (x ⁻¹)) ≈ e))

---------------------------------------------------------------------------------------------------------
--action associative
---------------------------------------------------------------------------------------------------------

p₁p₂Act : {P S : Set}{_∙_ : Op₂ P}{_≈_ : Rel S}{Act : P → S → S} → Set
p₁p₂Act {P}{S}{_∙_}{_≈_}{Act} = ∀ (p₁ p₂ : P) → ( ∀ {s : S} → Act p₁ (Act p₂ s) ≈ Act (p₂ ∙ p₁) s)


---------------------------------------------------------------------------------------------------------
--action identity
---------------------------------------------------------------------------------------------------------

ιAct : {P S : Set}{_≈_ : Rel S}{Act : P → S → S} → (ι : P) → Set  
ιAct {P}{S}{_≈_}{Act} ι = ∀ {s : S} → Act ι s ≈ s 


------------------------------------------------------------------------------------------------------------------------------
                                                 --List operations
------------------------------------------------------------------------------------------------------------------------------

[_] : {A : Set} → A → List A
[ x ] = x :: []


_++_ : {A : Set} → List A → List A → List A 
[]  ++ list₂  = list₂
(an_elem :: the_rest)  ++ list₂  = an_elem :: (the_rest ++ list₂)


---------------------------------------------------------------------------------------------------------------------------
                                          --Miscellaneous
---------------------------------------------------------------------------------------------------------------------------

---------------------------------------------------------------------
--≠
--------------------------------------------------------------------

_≠_ : {A : Set}(x x' : A) → Set 
x ≠ x' = (x ≡ x' → ⊥)

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