1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
{-# OPTIONS --without-K --safe #-}
module Data.Setoid where
open import Data.Product using (_,_)
open import Data.Product.Function.NonDependent.Setoid using (_×-function_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Function using (Func; _⟶ₛ_)
open import Function.Construct.Setoid using () renaming (setoid to infixr 0 _⇒ₛ_) public
open import Level using (Level)
open import Relation.Binary using (Setoid)
open Setoid renaming (Carrier to ∣_∣) public
open Func
_×-⇒_
: {c₁ c₂ c₃ c₄ c₅ c₆ : Level}
{ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level}
{A : Setoid c₁ ℓ₁}
{B : Setoid c₂ ℓ₂}
{C : Setoid c₃ ℓ₃}
{D : Setoid c₄ ℓ₄}
{E : Setoid c₅ ℓ₅}
{F : Setoid c₆ ℓ₆}
→ A ⟶ₛ B ⇒ₛ C
→ D ⟶ₛ E ⇒ₛ F
→ A ×ₛ D ⟶ₛ B ×ₛ E ⇒ₛ C ×ₛ F
_×-⇒_ f g .to (x , y) = to f x ×-function to g y
_×-⇒_ f g .cong (x , y) = cong f x , cong g y
assocₛ⇒
: {c₁ c₂ c₃ : Level}
{ℓ₁ ℓ₂ ℓ₃ : Level}
{A : Setoid c₁ ℓ₁}
{B : Setoid c₂ ℓ₂}
{C : Setoid c₃ ℓ₃}
→ (A ×ₛ B) ×ₛ C ⟶ₛ A ×ₛ (B ×ₛ C)
assocₛ⇒ .to ((x , y) , z) = x , (y , z)
assocₛ⇒ .cong ((≈x , ≈y) , ≈z) = ≈x , (≈y , ≈z)
assocₛ⇐
: {c₁ c₂ c₃ : Level}
{ℓ₁ ℓ₂ ℓ₃ : Level}
{A : Setoid c₁ ℓ₁}
{B : Setoid c₂ ℓ₂}
{C : Setoid c₃ ℓ₃}
→ A ×ₛ (B ×ₛ C) ⟶ₛ (A ×ₛ B) ×ₛ C
assocₛ⇐ .to (x , (y , z)) = (x , y) , z
assocₛ⇐ .cong (≈x , (≈y , ≈z)) = (≈x , ≈y) , ≈z
|
