{-# OPTIONS --without-K #-}
open import Agda.Primitive
open import 1-equality
open import 2-composition
open import 3-ap
Ω[_,_] :
{ℓ : Level} →
(A : Set ℓ) →
(a : A) →
Set ℓ
Ω[ A , a ] = a ≡ a
Ω²[_,_] :
{ℓ : Level} →
(A : Set ℓ) →
(a : A) →
Set ℓ
Ω²[ A , a ] = Ω[ Ω[ A , a ] , refl ]
Theorem·2·1·6 :
{ℓ : Level} →
(A : Set ℓ) →
(a : A) →
(α β : Ω²[ A , a ]) →
α • β ≡ β • α
Theorem·2·1·6 A a α β =
α•β≡α⋆β • α⋆β≡α⋆'β • α⋆'β≡β•α
where
_•₁_ :
{ℓ : Level} →
{A : Set ℓ} →
{a b c : A} →
{p q : a ≡ b} →
(α : p ≡ q) →
(r : b ≡ c) →
(p • r ≡ q • r)
α •₁ refl = sym(ru _) • α • (ru _)
_•₂_ :
{ℓ : Level} →
{A : Set ℓ} →
{a b c : A} →
{r s : b ≡ c} →
(q : a ≡ b) →
(β : r ≡ s) →
(q • r ≡ q • s)
refl •₂ β = sym(lu _) • β • (lu _)
_⋆_ :
{ℓ : Level} →
{A : Set ℓ} →
{a b c : A} →
{p q : a ≡ b} →
{r s : b ≡ c} →
(α : p ≡ q) →
(β : r ≡ s) →
(p • r ≡ q • s)
α ⋆ β = (α •₁ _) • (_ •₂ β)
_⋆'_ :
{ℓ : Level} →
{A : Set ℓ} →
{a b c : A} →
{p q : a ≡ b} →
{r s : b ≡ c} →
(α : p ≡ q) →
(β : r ≡ s) →
(p • r ≡ q • s)
α ⋆' β = (_ •₂ β) • (α •₁ _)
α•β≡α⋆β : α • β ≡ α ⋆ β
α•β≡α⋆β =
ap (λ x → α • x )
(lu β • ru (refl • β))
•
ap (λ x → x • (refl • β • refl))
(lu α • ru (refl • α))
α⋆β≡α⋆'β : α ⋆ β ≡ α ⋆' β
α⋆β≡α⋆'β = ⋆≡⋆' α β where
⋆≡⋆' :
{ℓ : Level} →
{A : Set ℓ} →
{a b c : A} →
{p q : a ≡ b} →
{r s : b ≡ c} →
(α : p ≡ q) →
(β : r ≡ s) →
(α ⋆ β ≡ α ⋆' β)
⋆≡⋆' {p = refl} {q = refl}
{r = refl} {s = refl}
refl refl = refl
α⋆'β≡β•α : α ⋆' β ≡ β • α
α⋆'β≡β•α =
sym ((ap (λ x → β • x )
(lu α • ru (refl • α)))
•
(ap (λ x → x • (refl • α • refl))
(lu β • ru (refl • β))))