```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' → ⊥)

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

```