{-# OPTIONS --without-K #-}
open import Agda.Primitive
open import 1-equality
open import 2-composition
open import 3-ap

-- Eckmann-Hilton Argument

-- Loop space

Ω[_,_] :
  { : 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 : --Eckmann-Hilton
  --                    Argument
  { : 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  β))))