module Palmse.Monoid.Pentagon (A : Set) where import Palmse.Monoid.Exp; open Palmse.Monoid.Exp A import Palmse.Monoid.Laws; open Palmse.Monoid.Laws A import Relation.Binary.EqReasoning as Reason open module R {A : Set} = Reason (ExpSetoid A) ass4 : {A : Set} -> (e₀ e₁ e₂ e₃ : Exp) -> ((e₀ ○ e₁) ○ e₂) ○ e₃ ∼ e₀ ○ (e₁ ○ (e₂ ○ e₃)) ass4 e₀ e₁ e₂ e₃ = -- tra ass ass begin ((e₀ ○ e₁) ○ e₂) ○ e₃ ≈⟨ ass ⟩ (e₀ ○ e₁) ○ (e₂ ○ e₃) ≈⟨ ass ⟩ e₀ ○ (e₁ ○ (e₂ ○ e₃)) ∎ -- \qed ass4' : {A : Set} -> (e₀ e₁ e₂ e₃ : Exp) -> ((e₀ ○ e₁) ○ e₂) ○ e₃ ∼ e₀ ○ (e₁ ○ (e₂ ○ e₃)) ass4' e₀ e₁ e₂ e₃ = begin ((e₀ ○ e₁) ○ e₂) ○ e₃ ≈⟨ fun ass ref ⟩ (e₀ ○ (e₁ ○ e₂)) ○ e₃ ≈⟨ ass ⟩ e₀ ○ ((e₁ ○ e₂) ○ e₃) ≈⟨ fun ref ass ⟩ e₀ ○ (e₁ ○ (e₂ ○ e₃)) ∎ -- a critical pair: two ways of reducing ((e₀ ○ e₁) ○ e₂) ○ e₃ -- Cf also Mac Lane's pentagon coherence condition for monoidal categories