open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Level
open import Data.Product using (Σ ; proj₁ ; proj₂ ; _×_ ; _,_)
Σ∶• : {a b : Level} (A : Set a) (B : A → Set b) → Set (a ⊔ b)
Σ∶• = Σ
infix -666 Σ∶•
syntax Σ∶• A (λ x → B) = Σ x ∶ A • B
record Semigroup0 : Set₁ where
field
Carrier : Set
_⨾_ : Carrier → Carrier → Carrier
assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)
record Semigroup1 (Carrier : Set): Set₁ where
field
_⨾_ : Carrier → Carrier → Carrier
assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)
record Semigroup2
(Carrier : Set)
(_⨾_ : Carrier → Carrier → Carrier) : Set where
field
assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)
record Semigroup3
(Carrier : Set)
(_⨾_ : Carrier → Carrier → Carrier)
(assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)) : Set where
Surjection : ∀{A B : Set} → (A → B) → Set
Surjection {A} {B} f = ∀ (b : B) → Σ a ∶ A • b ≡ f a
Injection : ∀{A B : Set} → (A → B) → Set
Injection {A} {B} f = ∀ {x y} → f x ≡ f y → x ≡ y
translate1 : ∀{A B} → (f : A → B) → Surjection f → Injection f
→ Semigroup1 A → Semigroup1 B
translate1 f surj inj AS =
let
open Semigroup1 AS
infix 5 _⨾′_
_⨾′_ = λ x y → let a0 = proj₁ (surj x); a1 = proj₁ (surj y) in f (a0 ⨾ a1)
factor : ∀ {a a′} → f a ⨾′ f a′ ≡ f (a ⨾ a′)
factor {a} {a′} =
let 𝒶 , m = surj (f a)
𝒶′ , w = surj (f a′)
in
begin
f a ⨾′ f a′
≡⟨ refl ⟩
f (𝒶 ⨾ 𝒶′)
≡⟨ cong f (cong₂ _⨾_ (inj (sym m)) (inj (sym w))) ⟩
f (a ⨾ a′)
∎
distribute : ∀ {a a′} → f (a ⨾ a′) ≡ f a ⨾′ f a′
distribute {a} {a′} = sym (factor {a} {a′})
in
record { _⨾_ = _⨾′_; assoc = λ x y z →
let
a₀ , x≈fa₀ = surj x
a₁ , y≈fa₁ = surj y
a₂ , z≈fa₂ = surj z
in
begin
(x ⨾′ y) ⨾′ z
≡⟨ cong₂ _⨾′_ (cong₂ _⨾′_ x≈fa₀ y≈fa₁) z≈fa₂ ⟩
(f a₀ ⨾′ f a₁) ⨾′ f a₂
≡⟨ cong (_⨾′ f a₂) factor ⟩
f (a₀ ⨾ a₁) ⨾′ f a₂
≡⟨ factor ⟩
f ((a₀ ⨾ a₁) ⨾ a₂)
≡⟨ cong f (assoc _ _ _) ⟩
f (a₀ ⨾ (a₁ ⨾ a₂))
≡⟨ distribute ⟩
f a₀ ⨾′ f (a₁ ⨾ a₂)
≡⟨ cong (f a₀ ⨾′_) distribute ⟩
f a₀ ⨾′ (f a₁ ⨾′ f a₂)
≡⟨ sym (cong₂ _⨾′_ x≈fa₀ (cong₂ _⨾′_ y≈fa₁ z≈fa₂)) ⟩
x ⨾′ (y ⨾′ z)
∎
}
translate0 : ∀{B : Set} (AS : Semigroup0) (f : Semigroup0.Carrier AS → B)
→ Surjection f → Injection f
→ Semigroup0
translate0 {B} AS f surj inj = record { Carrier = B ; _⨾_ = _⨾_ ; assoc = assoc }
where
pack : Semigroup1 (Semigroup0.Carrier AS)
pack = let open Semigroup0 AS
in record {_⨾_ = _⨾_; assoc = assoc }
open Semigroup1 (translate1 f surj inj pack)