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}