Chuangjie Xu 2012 (updated in February 2015)

\begin{code}

{-# OPTIONS --without-K #-}

module UsingSetoid.Setoid where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence

\end{code}

Setoids and E-maps

\begin{code}

isEqRel : {A : Set} → (A → A → Set) → Set
isEqRel R =   (∀ a → R a a)
            × (∀ a a' → R a a' → R a' a)
            × (∀ a₀ a₁ a₂ → R a₀ a₁ → R a₁ a₂ → R a₀ a₂)

Setoid : Set₁
Setoid = Σ \(A : Set) → Σ \(R : A → A → Set) → isEqRel R

E-map : Setoid → Setoid → Set
E-map (A , _~_ , _) (B , _≈_ , _) =
   Σ \(f : A → B) → ∀ a a' → a ~ a' → f a ≈ f a'

⟨_∣_∣_⟩_◎_ : (A B C : Setoid) → E-map B C → E-map A B → E-map A C
⟨ A ∣ B ∣ C ⟩ (g , eg) ◎ (f , ef) = g ∘ f , (λ a a' e → eg (f a) (f a') (ef a a' e))

E-id : (A : Setoid) → E-map A A
E-id A = id , (λ _ _ e → e) 

U = pr₁

E : (A : Setoid) → U A → U A → Set
E (_ , _~_ , _) = _~_

Refl : (A : Setoid) → ∀(a : U A) → E A a a
Refl (_ , _ , r , _) = r

Sym : (A : Setoid) → ∀(a a' : U A) → E A a a' → E A a' a
Sym (_ , _ , _ , s , _) = s

Trans : (A : Setoid) → ∀(a₀ a₁ a₂ : U A) → E A a₀ a₁ → E A a₁ a₂ → E A a₀ a₂
Trans (_ , _ , _ , _ , t) = t

\end{code}

Product

\begin{code}

infixl 4 _✻_

_✻_ : Setoid → Setoid → Setoid
(A , _~_ , rA , sA , tA) ✻ (B , _≈_ , rB , sB , tB) =
            (A × B , _≋_ , rC , sC , tC)
 where
  _≋_ : A × B → A × B → Set
  (a , b) ≋ (a' , b') = (a ~ a') × (b ≈ b')
  rC : ∀(c : A × B) → c ≋ c
  rC (a , b) = rA a , rB b
  sC : ∀(c c' : A × B) → c ≋ c' → c' ≋ c
  sC (a , b) (a' , b') (ea , eb) = sA a a' ea , sB b b' eb
  tC : ∀(c₀ c₁ c₂ : A × B) → c₀ ≋ c₁ → c₁ ≋ c₂ → c₀ ≋ c₂
  tC (a₀ , b₀) (a₁ , b₁) (a₂ , b₂) (ea , eb) (ea' , eb') =
     tA a₀ a₁ a₂ ea ea' , tB b₀ b₁ b₂ eb eb'

E-pr₁ : (A B : Setoid) → E-map (A ✻ B) A
E-pr₁ A B = pr₁ , (λ _ _ e → pr₁ e)

E-pr₂ : (A B : Setoid) → E-map (A ✻ B) B
E-pr₂ A B = pr₂ , (λ _ _ e → pr₂ e)

\end{code}

Function space

\begin{code}

infixl 4 _➡_

_➡_ : Setoid → Setoid → Setoid
X ➡ Y = (E-map X Y , _≋_ , rC , sC , tC)
 where
  A : Set
  A = U X
  B : Set
  B = U Y
  _≈_ : B → B → Set
  _≈_ = E Y
  rB : ∀(b : B) → b ≈ b
  rB = pr₁ (pr₂ (pr₂ Y))
  sB : ∀(b b' : B) → b ≈ b' → b' ≈ b
  sB = pr₁ (pr₂ (pr₂ (pr₂ Y)))
  tB : ∀(b₀ b₁ b₂ : B) → b₀ ≈ b₁ → b₁ ≈ b₂ → b₀ ≈ b₂
  tB = pr₂ (pr₂ (pr₂ (pr₂ Y)))
  _≋_ : E-map X Y → E-map X Y → Set
  (f , _) ≋ (g , _) = ∀(a : A) → f a ≈ g a
  rC : ∀(c : E-map X Y) → c ≋ c
  rC (f , _) = λ a → rB (f a)
  sC : ∀(c c' : E-map X Y) → c ≋ c' → c' ≋ c
  sC (f , _) (f' , _) eq = λ a → sB (f a) (f' a) (eq a)
  tC : ∀(c₀ c₁ c₂ : E-map X Y) → c₀ ≋ c₁ → c₁ ≋ c₂ → c₀ ≋ c₂
  tC (f₀ , _) (f₁ , _) (f₂ , _) eq eq' = λ a → tB (f₀ a) (f₁ a) (f₂ a) (eq a) (eq' a)

\end{code}

Initial and terminal setoids

\begin{code}

≡-isEqRel : ∀{A : Set} → isEqRel {A} (_≡_ {A = A})
≡-isEqRel = (λ _ → refl) ,
            (λ _ _ p → p ⁻¹) ,
            (λ _ _ _ p p' → p · p')

E∅ : Setoid
E∅ = ∅ , _≡_ , ≡-isEqRel

E⒈ : Setoid
E⒈ = ⒈ , _≡_ , ≡-isEqRel

E-unit : {A : Setoid} → E-map A E⒈
E-unit = unit , λ _ _ _ → refl

\end{code}

Objects of natural numbers and booleans

\begin{code}

Eℕ : Setoid
Eℕ = ℕ , _≡_ , ≡-isEqRel

E₂ : Setoid
E₂ = ₂ , _≡_ , ≡-isEqRel

\end{code}

The internal cantor space

\begin{code}

≣-isEqRel : isEqRel _≣_
≣-isEqRel = (λ _ _ → refl) ,
            (λ _ _ f i → (f i)⁻¹) ,
            (λ _ _ _ f g i → (f i) · (g i))

E₂ℕ : Setoid
E₂ℕ = ₂ℕ , _≣_ , ≣-isEqRel

Lemma[₂ℕ-E-map] : ∀(α : ₂ℕ) → ∀ i j → i ≡ j → α i ≡ α j
Lemma[₂ℕ-E-map] α i j p = ap α p

E-map-₂ℕ : Setoid → Set
E-map-₂ℕ A = E-map E₂ℕ A

E-map-₂ℕ-₂ℕ : Set
E-map-₂ℕ-₂ℕ = E-map E₂ℕ E₂ℕ

⟨_∣_⟩_◎_ : (B C : Setoid) → E-map B C → E-map-₂ℕ B → E-map-₂ℕ C
⟨_∣_⟩_◎_ B C f p = ⟨ E₂ℕ ∣ B ∣ C ⟩ f ◎ p

⟨_⟩_◎_ : (C : Setoid) → E-map-₂ℕ C → E-map-₂ℕ-₂ℕ → E-map-₂ℕ C
⟨_⟩_◎_ C p t = ⟨ E₂ℕ ∣ C ⟩ p ◎ t

infixl 30 _◎_

_◎_ : E-map E₂ℕ E₂ℕ → E-map-₂ℕ-₂ℕ → E-map-₂ℕ-₂ℕ
t ◎ r  = ⟨ E₂ℕ ⟩ t ◎ r

cons-E-map : ∀ {n} → (s : ₂Fin n) → ∀ α β
           → α ≣ β → cons s α ≣ cons s β
cons-E-map ⟨⟩      α β e  i       = e i
cons-E-map (b ∷ _) α β e  0       = refl
cons-E-map (_ ∷ s) α β e (succ i) = cons-E-map s α β e i

Cons : {n : ℕ} → ₂Fin n → E-map-₂ℕ-₂ℕ
Cons s = cons s , cons-E-map s

E-λα : (A : Setoid) → U A → E-map-₂ℕ A
E-λα A a = (λ α → a) , (λ _ _ _ → Refl A a)

\end{code}