From e0845b2562ca48a2169081ce3f69ce3d5c84eb5d Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 3 May 2021 17:41:32 -0700 Subject: [PATCH 1/7] Start work on a monoidal category solver --- src/Categories/Tactic/Monoidal.agda | 260 ++++++++++++++++++++++++++++ 1 file changed, 260 insertions(+) create mode 100644 src/Categories/Tactic/Monoidal.agda diff --git a/src/Categories/Tactic/Monoidal.agda b/src/Categories/Tactic/Monoidal.agda new file mode 100644 index 000000000..6fe1f6f70 --- /dev/null +++ b/src/Categories/Tactic/Monoidal.agda @@ -0,0 +1,260 @@ +{-# OPTIONS --without-K --safe #-} + +-- A Solver for monoidal categories. +-- Roughly based off of "Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids", +-- by Ilya Beylin and Peter Dybjer. +module Categories.Tactic.Monoidal where + +open import Level +open import Data.Product using (_,_) + +open import Relation.Binary.PropositionalEquality + +open import Categories.Category.Core using (Category) +open import Categories.Category.Monoidal.Core using (Monoidal) + +import Categories.Morphism.Reasoning as MR + +-------------------------------------------------------------------------------- +-- Introduction: +-- The basic idea of this solver is similar to a coherence theorem for +-- monoidal categories. We are going to show that every single +-- chain of coherence morphisms have some canonical form. +-- Once we have done that, it is simply a matter of mapping two +-- chains of coherence morphisms to their normal forms, and checking +-- if the two are equal. + +module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where + + infixr 9 _∘′_ + + infixr 10 _⊗₀′_ _⊗₁′_ + + open Category 𝒞 + open Monoidal 𝒱 + + open HomReasoning + open MR 𝒞 + + -------------------------------------------------------------------------------- + -- A 'Word' reifies all the parenthesis/tensors/units of some object + -- in a monoidal category into a data structure + -------------------------------------------------------------------------------- + data Word : Set o where + _⊗₀′_ : Word → Word → Word + unit′ : Word + _′ : Obj → Word + + reify : Word → Obj + reify (w₁ ⊗₀′ w₂) = reify w₁ ⊗₀ reify w₂ + reify unit′ = unit + reify (x ′) = x + + private + variable + X Y Z : Obj + A B C D : Word + + -------------------------------------------------------------------------------- + -- An 'Expr' reifies all unitors, associators and their compositions + -- into a data structure. + -------------------------------------------------------------------------------- + data Expr : Word → Word → Set (o ⊔ ℓ) where + id′ : Expr A A + _∘′_ : Expr B C → Expr A B → Expr A C + _⊗₁′_ : Expr A C → Expr B D → Expr (A ⊗₀′ B) (C ⊗₀′ D) + α′ : Expr ((A ⊗₀′ B) ⊗₀′ C) (A ⊗₀′ (B ⊗₀′ C)) + α⁻¹′ : Expr (A ⊗₀′ (B ⊗₀′ C)) ((A ⊗₀′ B) ⊗₀′ C) + ƛ′ : Expr (unit′ ⊗₀′ A) A + ƛ⁻¹′ : Expr A (unit′ ⊗₀′ A) + ρ′ : Expr (A ⊗₀′ unit′) A + ρ⁻¹′ : Expr A (A ⊗₀′ unit′) + + -- Embed a morphism in 'Expr' back into '𝒞' without normalizing. + [_↓] : Expr A B → (reify A) ⇒ (reify B) + [ id′ ↓] = id + [ f ∘′ g ↓] = [ f ↓] ∘ [ g ↓] + [ f ⊗₁′ g ↓] = [ f ↓] ⊗₁ [ g ↓] + [ α′ ↓] = associator.from + [ α⁻¹′ ↓] = associator.to + [ ƛ′ ↓] = unitorˡ.from + [ ƛ⁻¹′ ↓] = unitorˡ.to + [ ρ′ ↓] = unitorʳ.from + [ ρ⁻¹′ ↓] = unitorʳ.to + + -- Invert a composition of coherence morphisms + invert : Expr A B → Expr B A + invert id′ = id′ + invert (f ∘′ g) = invert g ∘′ invert f + invert (f ⊗₁′ g) = invert f ⊗₁′ invert g + invert α′ = α⁻¹′ + invert α⁻¹′ = α′ + invert ƛ′ = ƛ⁻¹′ + invert ƛ⁻¹′ = ƛ′ + invert ρ′ = ρ⁻¹′ + invert ρ⁻¹′ = ρ′ + + -- Reassociate all the tensors to the right. + -- + -- Note [reassoc + lists]: + -- We could use a list here, but this version is somewhat nicer, + -- as we can get things like right-identity for free. + reassoc : Word → (Word → Word) + reassoc (w₁ ⊗₀′ w₂) rest = reassoc w₁ (reassoc w₂ rest) + reassoc unit′ rest = rest + reassoc (x ′) rest = (x ′) ⊗₀′ rest + + -- This is the key proof of the entire tactic. + -- 'coherence e' proves that all of our coherence morphisms + -- in 'e' are not required after reassociation, as they are on-the-nose equal. + coherence : Expr A B → (X : Word) → reassoc A X ≡ reassoc B X + coherence id′ X = refl + coherence (f ∘′ g) X = trans (coherence g X) (coherence f X) + coherence (_⊗₁′_ {A} {B} {C} {D} f g) X = trans (cong (reassoc A) (coherence g X)) (coherence f (reassoc D X)) + coherence α′ X = refl + coherence α⁻¹′ X = refl + coherence ƛ′ X = refl + coherence ƛ⁻¹′ X = refl + coherence ρ′ X = refl + coherence ρ⁻¹′ X = refl + + -- Place every word into a normal form + -- > nf ((W ′ ⊗₀′ X ′) ⊗₀′ (Y ′ ⊗₀′ Z ′)) + -- W ′ ⊗₀ X ′ ⊗₀ Y ′ ⊗₀ Z ′ ⊗₀ unit′ + nf : Word → Word + nf w = reassoc w unit′ + + -- Given some coherence morphism, build a morphisms between + -- the normal forms of it's domain and codomain. + -- This will be equal to the identity morphism. + strict : Expr A B → Expr (nf A) (nf B) + strict {A = A} {B = B} e = subst (λ X → Expr (reassoc A unit′) X) (coherence e unit′) id′ + + -- If we reassociate and tensor after that, we can find some coherence + -- morphism that removes the pointless unit. + slurp : ∀ (A B : Word) → Expr (reassoc A unit′ ⊗₀′ B) (reassoc A B) + slurp (A ⊗₀′ B) C = slurp A (reassoc B C) ∘′ (id′ ⊗₁′ slurp B C) ∘′ α′ ∘′ (invert (slurp A (reassoc B unit′) ⊗₁′ id′)) + slurp unit′ B = ƛ′ + slurp (x ′) B = ρ′ ⊗₁′ id′ + + -- Coherence morphism witnessing the concatentation of normal forms. + nf-homo : ∀ (A B : Word) → Expr (nf A ⊗₀′ nf B) (nf (A ⊗₀′ B)) + nf-homo A B = slurp A (reassoc B unit′) + + -- Build a coherence morphism out of some word into it's normal form. + into : ∀ (A : Word) → Expr A (nf A) + into (A ⊗₀′ B) = nf-homo A B ∘′ (into A ⊗₁′ into B) + into unit′ = id′ + into (x ′) = ρ⁻¹′ + + -- Build a coherence morphism into a word from it's normal form. + out : ∀ (A : Word) → Expr (nf A) A + out A = invert (into A) + + -- Normalize an expression. + -- We do this by building maps into and out of the normal forms of the + -- domain/codomain, then using our 'strict' coherence morphism to link them together. + normalize : Expr A B → Expr A B + normalize {A = A} {B = B} f = out B ∘′ strict f ∘′ into A + + -- Witness the isomorphism between 'f' and 'invert f'. + invert-isoˡ : ∀ (f : Expr A B) → [ invert f ↓] ∘ [ f ↓] ≈ id + invert-isoˡ id′ = identity² + invert-isoˡ (f ∘′ g) = begin + ([ invert g ↓] ∘ [ invert f ↓]) ∘ ([ f ↓] ∘ [ g ↓]) ≈⟨ cancelInner (invert-isoˡ f) ⟩ + [ invert g ↓] ∘ [ g ↓] ≈⟨ invert-isoˡ g ⟩ + id ∎ + invert-isoˡ (f ⊗₁′ g) = begin + ([ invert f ↓] ⊗₁ [ invert g ↓]) ∘ ([ f ↓] ⊗₁ [ g ↓]) ≈˘⟨ ⊗.homomorphism ⟩ + ([ invert f ↓] ∘ [ f ↓]) ⊗₁ ([ invert g ↓] ∘ [ g ↓]) ≈⟨ ⊗.F-resp-≈ (invert-isoˡ f , invert-isoˡ g) ⟩ + id ⊗₁ id ≈⟨ ⊗.identity ⟩ + id ∎ + invert-isoˡ α′ = associator.isoˡ + invert-isoˡ α⁻¹′ = associator.isoʳ + invert-isoˡ ƛ′ = unitorˡ.isoˡ + invert-isoˡ ƛ⁻¹′ = unitorˡ.isoʳ + invert-isoˡ ρ′ = unitorʳ.isoˡ + invert-isoˡ ρ⁻¹′ = unitorʳ.isoʳ + + -- Witness the isomorphism between 'f' and 'invert f'. + invert-isoʳ : ∀ (f : Expr A B) → [ f ↓] ∘ [ invert f ↓] ≈ id + invert-isoʳ id′ = identity² + invert-isoʳ (f ∘′ g) = begin + ([ f ↓] ∘ [ g ↓]) ∘ ([ invert g ↓] ∘ [ invert f ↓]) ≈⟨ cancelInner (invert-isoʳ g) ⟩ + [ f ↓] ∘ [ invert f ↓] ≈⟨ invert-isoʳ f ⟩ + id ∎ + invert-isoʳ (f ⊗₁′ g) = begin + ([ f ↓] ⊗₁ [ g ↓]) ∘ ([ invert f ↓] ⊗₁ [ invert g ↓]) ≈˘⟨ ⊗.homomorphism ⟩ + ([ f ↓] ∘ [ invert f ↓]) ⊗₁ ([ g ↓] ∘ [ invert g ↓]) ≈⟨ ⊗.F-resp-≈ (invert-isoʳ f , invert-isoʳ g) ⟩ + id ⊗₁ id ≈⟨ ⊗.identity ⟩ + id ∎ + invert-isoʳ α′ = associator.isoʳ + invert-isoʳ α⁻¹′ = associator.isoˡ + invert-isoʳ ƛ′ = unitorˡ.isoʳ + invert-isoʳ ƛ⁻¹′ = unitorˡ.isoˡ + invert-isoʳ ρ′ = unitorʳ.isoʳ + invert-isoʳ ρ⁻¹′ = unitorʳ.isoˡ + + -- Helper lemma for showing that mapping into a normal form then back out + -- is identity. + into-out : ∀ (A : Word) → [ out A ↓] ∘ id ∘ [ into A ↓] ≈ id + into-out A = begin + [ out A ↓] ∘ id ∘ [ into A ↓] ≈⟨ refl⟩∘⟨ identityˡ ⟩ + [ out A ↓] ∘ [ into A ↓] ≈⟨ invert-isoˡ (into A) ⟩ + id ∎ + + -- Slurping on a unit is the same as removing the redundant unit by using + -- the right associator. + slurp-unit : ∀ (A : Word) → [ slurp A unit′ ↓] ≈ [ ρ′ {reassoc A unit′} ↓] + slurp-unit (A ⊗₀′ A₁) = {!!} + slurp-unit unit′ = {!!} + slurp-unit (x ′) = {!!} + + -- The strict coherence morphism of a composition is the composition of the strict morphisms. + strict-∘ : ∀ (f : Expr B C) (g : Expr A B) → [ strict (f ∘′ g) ↓] ≈ [ strict f ↓] ∘ [ strict g ↓] + strict-∘ f g rewrite (coherence g unit′) | (coherence f unit′) = Equiv.sym identity² + + -- For whatever reason this is HARD TO PROVE. + -- We run into all sorts of crazy issues when we try to rewrite any of the 'coherence f' proofs. + strict-⊗ : ∀ (f : Expr A C) (g : Expr B D) → [ strict (f ⊗₁′ g) ↓] ≈ [ (nf-homo C D) ↓] ∘ [ strict f ↓] ⊗₁ [ strict g ↓] ∘ [ invert (nf-homo A B) ↓] + strict-⊗ {A} {C} {B} {D} f g = {!!} + + -- Normalization preserves equality. + preserves-≈ : ∀ (f : Expr A B) → [ normalize f ↓] ≈ [ f ↓] + preserves-≈ (id′ {A}) = into-out A + preserves-≈ (_∘′_ {B} {C} {A} f g) = begin + [ out C ↓] ∘ [ strict (f ∘′ g) ↓] ∘ [ into A ↓] ≈⟨ refl⟩∘⟨ strict-∘ f g ⟩∘⟨refl ⟩ + [ out C ↓] ∘ ([ strict f ↓] ∘ [ strict g ↓]) ∘ [ into A ↓] ≈˘⟨ refl⟩∘⟨ cancelInner (invert-isoʳ (into B)) ⟩∘⟨refl ⟩ + [ out C ↓] ∘ (([ strict f ↓] ∘ [ into B ↓]) ∘ ([ out B ↓] ∘ [ strict g ↓])) ∘ [ into A ↓] ≈⟨ center⁻¹ (preserves-≈ f) (assoc ○ preserves-≈ g) ⟩ + [ f ↓] ∘ [ g ↓] ∎ + preserves-≈ (_⊗₁′_ {A} {C} {B} {D} f g) = begin + ([ out C ↓] ⊗₁ [ out D ↓] ∘ [ invert (nf-homo C D) ↓]) ∘ [ strict (f ⊗₁′ g) ↓] ∘ [ nf-homo A B ↓] ∘ [ into A ↓] ⊗₁ [ into B ↓] + ≈⟨ refl⟩∘⟨ strict-⊗ f g ⟩∘⟨refl ⟩ + ([ out C ↓] ⊗₁ [ out D ↓] ∘ [ invert (nf-homo C D) ↓]) ∘ ([ (nf-homo C D) ↓] ∘ [ strict f ↓] ⊗₁ [ strict g ↓] ∘ [ invert (nf-homo A B) ↓]) ∘ [ nf-homo A B ↓] ∘ [ into A ↓] ⊗₁ [ into B ↓] + ≈⟨ {!!} ⟩ + [ out C ↓] ⊗₁ [ out D ↓] ∘ [ strict f ↓] ⊗₁ [ strict g ↓] ∘ [ into A ↓] ⊗₁ [ into B ↓] + ≈⟨ {!!} ⟩ + ([ out C ↓] ∘ [ strict f ↓] ∘ [ into A ↓]) ⊗₁ ([ out D ↓] ∘ [ strict g ↓] ∘ [ into B ↓]) + ≈⟨ ⊗.F-resp-≈ (preserves-≈ f , preserves-≈ g) ⟩ + [ f ↓] ⊗₁ [ g ↓] ∎ + preserves-≈ (α′ {A} {B} {C}) = begin + ([ invert (into A) ↓] ⊗₁ ([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓] ∘ [ invert (nf-homo B C) ↓]) ∘ [ invert (nf-homo A (B ⊗₀′ C)) ↓]) ∘ id ∘ ([ slurp A (reassoc B (reassoc C unit′)) ↓] ∘ id ⊗₁ [ slurp B (reassoc C unit′) ↓] ∘ associator.from ∘ [ invert (slurp A (reassoc B unit′)) ↓] ⊗₁ id) ∘ ([ nf-homo A B ↓] ∘ [ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓] ≈⟨ {!!} ⟩ + associator.from ∎ + preserves-≈ α⁻¹′ = {!!} + preserves-≈ (ƛ′ {A}) = begin + [ out A ↓] ∘ id ∘ unitorˡ.from ∘ id ⊗₁ [ into A ↓] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-from ⟩ + [ out A ↓] ∘ id ∘ [ into A ↓] ∘ unitorˡ.from ≈˘⟨ assoc²' ⟩ + ([ out A ↓] ∘ id ∘ [ into A ↓]) ∘ unitorˡ.from ≈⟨ elimˡ (into-out A) ⟩ + unitorˡ.from ∎ + preserves-≈ (ƛ⁻¹′ {A}) = begin + (id ⊗₁ [ out A ↓] ∘ unitorˡ.to) ∘ id ∘ [ into A ↓] ≈˘⟨ unitorˡ-commute-to ⟩∘⟨refl ⟩ + (unitorˡ.to ∘ [ out A ↓]) ∘ id ∘ [ into A ↓] ≈⟨ cancelʳ (into-out A) ⟩ + unitorˡ.to ∎ + preserves-≈ (ρ′ {A}) = begin + [ out A ↓] ∘ id ∘ [ slurp A unit′ ↓] ∘ ([ into A ↓] ⊗₁ id) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (slurp-unit A ⟩∘⟨refl) ⟩ + [ out A ↓] ∘ id ∘ unitorʳ.from ∘ ([ into A ↓] ⊗₁ id) ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ unitorʳ-commute-from) ⟩ + [ out A ↓] ∘ id ∘ [ into A ↓] ∘ unitorʳ.from ≈˘⟨ assoc²' ⟩ + ([ out A ↓] ∘ id ∘ [ into A ↓]) ∘ unitorʳ.from ≈⟨ elimˡ (into-out A) ⟩ + unitorʳ.from ∎ + preserves-≈ (ρ⁻¹′ {A}) = {!!} + From 27dc6adf0332a243747f83014b98fc3e7ee7786d Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Wed, 5 May 2021 01:41:07 +0200 Subject: [PATCH 2/7] WIP: reworked @TOTBWF's monoid solver. --- src/Categories/Tactic/Monoidal.agda | 327 ++++++++++++++++++++++++++++ 1 file changed, 327 insertions(+) create mode 100644 src/Categories/Tactic/Monoidal.agda diff --git a/src/Categories/Tactic/Monoidal.agda b/src/Categories/Tactic/Monoidal.agda new file mode 100644 index 000000000..af2e8ff95 --- /dev/null +++ b/src/Categories/Tactic/Monoidal.agda @@ -0,0 +1,327 @@ +{-# OPTIONS --without-K --safe #-} + +-- A Solver for monoidal categories. +-- Roughly based off of "Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids", +-- by Ilya Beylin and Peter Dybjer. +module Categories.Tactic.Monoidal where + +open import Level +open import Data.Product using (_,_) +open import Data.List +open import Data.List.Properties using (++-assoc; ++-identityʳ) + +open import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality.Properties + using (subst-application) + +open import Categories.Category.Core using (Category) +open import Categories.Category.Monoidal.Core using (Monoidal) +import Categories.Category.Monoidal.Reasoning as MonoidalReasoning +open import Categories.Category.Monoidal.Properties using (module Kelly's) + +import Categories.Morphism.Reasoning as MR + +-------------------------------------------------------------------------------- +-- Introduction: +-- The basic idea of this solver is similar to a coherence theorem for +-- monoidal categories. We are going to show that every single +-- chain of coherence morphisms have some canonical form. +-- Once we have done that, it is simply a matter of mapping two +-- chains of coherence morphisms to their normal forms, and checking +-- if the two are equal. + +module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where + + infixr 9 _∘′_ + + infixr 10 _⊗₀′_ _⊗₁′_ + + open Category 𝒞 + open Monoidal 𝒱 + + open MR 𝒞 + open MonoidalReasoning 𝒱 + + -------------------------------------------------------------------------------- + -- A 'Word' reifies all the parenthesis/tensors/units of some object + -- in a monoidal category into a data structure + -------------------------------------------------------------------------------- + data Word : Set o where + _⊗₀′_ : Word → Word → Word + unit′ : Word + _′ : (X : Obj) → Word + + reify : Word → Obj + reify (w₁ ⊗₀′ w₂) = reify w₁ ⊗₀ reify w₂ + reify unit′ = unit + reify (x ′) = x + + private + variable + X Y Z : Obj + A B C D : Word + + -------------------------------------------------------------------------------- + -- An 'Expr' reifies all unitors, associators and their compositions + -- into a data structure. + -------------------------------------------------------------------------------- + data Expr : Word → Word → Set o where + id′ : Expr A A + _∘′_ : Expr B C → Expr A B → Expr A C + _⊗₁′_ : Expr A C → Expr B D → Expr (A ⊗₀′ B) (C ⊗₀′ D) + α′ : Expr ((A ⊗₀′ B) ⊗₀′ C) (A ⊗₀′ (B ⊗₀′ C)) + α⁻¹′ : Expr (A ⊗₀′ (B ⊗₀′ C)) ((A ⊗₀′ B) ⊗₀′ C) + ƛ′ : Expr (unit′ ⊗₀′ A) A + ƛ⁻¹′ : Expr A (unit′ ⊗₀′ A) + ρ′ : Expr (A ⊗₀′ unit′) A + ρ⁻¹′ : Expr A (A ⊗₀′ unit′) + + -- Embed a morphism in 'Expr' back into '𝒞' without normalizing. + [_↓] : Expr A B → (reify A) ⇒ (reify B) + [ id′ ↓] = id + [ f ∘′ g ↓] = [ f ↓] ∘ [ g ↓] + [ f ⊗₁′ g ↓] = [ f ↓] ⊗₁ [ g ↓] + [ α′ ↓] = associator.from + [ α⁻¹′ ↓] = associator.to + [ ƛ′ ↓] = unitorˡ.from + [ ƛ⁻¹′ ↓] = unitorˡ.to + [ ρ′ ↓] = unitorʳ.from + [ ρ⁻¹′ ↓] = unitorʳ.to + + infix 4 _≈↓_ + + -- TODO: is this sufficient or should we define an equality directly + -- on Expr? + _≈↓_ : (f g : Expr A B) → Set e + f ≈↓ g = [ f ↓] ≈ [ g ↓] + + -- Invert a composition of coherence morphisms + invert : Expr A B → Expr B A + invert id′ = id′ + invert (f ∘′ g) = invert g ∘′ invert f + invert (f ⊗₁′ g) = invert f ⊗₁′ invert g + invert α′ = α⁻¹′ + invert α⁻¹′ = α′ + invert ƛ′ = ƛ⁻¹′ + invert ƛ⁻¹′ = ƛ′ + invert ρ′ = ρ⁻¹′ + invert ρ⁻¹′ = ρ′ + + NfWord : Set o + NfWord = List Obj + + data NfExpr : NfWord → NfWord → Set o where + id′ : ∀ {N} → NfExpr N N + + -- An embedding of normal forms + + ⌞_⌟ : NfWord → Word + ⌞ [] ⌟ = unit′ + ⌞ A ∷ N ⌟ = (A ′) ⊗₀′ ⌞ N ⌟ + + ⌊_⌋ : ∀ {N M} → NfExpr N M → Expr ⌞ N ⌟ ⌞ M ⌟ + ⌊ id′ ⌋ = id′ + + -- The monoidal operations are all admissible on normal forms. + + infixr 9 _∘ⁿ_ + infixr 10 _⊗ⁿ_ + + _∘ⁿ_ : ∀ {N₁ N₂ N₃} → + NfExpr N₂ N₃ → NfExpr N₁ N₂ → NfExpr N₁ N₃ + id′ ∘ⁿ id′ = id′ + + _⊗ⁿ_ : ∀ {N₁ N₂ M₁ M₂} → + NfExpr N₁ M₁ → NfExpr N₂ M₂ → NfExpr (N₁ ++ N₂) (M₁ ++ M₂) + id′ ⊗ⁿ id′ = id′ + + αⁿ : ∀ N₁ N₂ N₃ → NfExpr ((N₁ ++ N₂) ++ N₃) (N₁ ++ (N₂ ++ N₃)) + αⁿ N₁ N₂ N₃ = subst (NfExpr ((N₁ ++ N₂) ++ N₃)) (++-assoc N₁ N₂ N₃) id′ + + ρⁿ : ∀ N → NfExpr (N ++ []) N + ρⁿ N = subst (NfExpr (N ++ [])) (++-identityʳ N) id′ + + invertⁿ : ∀ {N M} → NfExpr N M → NfExpr M N + invertⁿ id′ = id′ + + -- The normalization functor + + nf₀ : Word → NfWord + nf₀ (A₁ ⊗₀′ A₂) = nf₀ A₁ ++ nf₀ A₂ + nf₀ unit′ = [] + nf₀ (X ′) = X ∷ [] + + nf₁ : Expr A B → NfExpr (nf₀ A) (nf₀ B) + nf₁ id′ = id′ + nf₁ (f ∘′ g) = nf₁ f ∘ⁿ nf₁ g + nf₁ (f ⊗₁′ g) = nf₁ f ⊗ⁿ nf₁ g + nf₁ (α′ {A} {B} {C}) = αⁿ (nf₀ A) (nf₀ B) (nf₀ C) + nf₁ (α⁻¹′ {A} {B} {C}) = invertⁿ (αⁿ (nf₀ A) (nf₀ B) (nf₀ C)) + nf₁ ƛ′ = id′ + nf₁ ƛ⁻¹′ = id′ + nf₁ ρ′ = ρⁿ _ + nf₁ ρ⁻¹′ = invertⁿ (ρⁿ _) + + -- The embedding is a monoidal functor + + ⌊⌋-id : ∀ {N} → ⌊ id′ {N} ⌋ ≈↓ id′ + ⌊⌋-id = Equiv.refl + + ⌊⌋-∘ : ∀ {N₁ N₂ N₃} (f : NfExpr N₂ N₃) (g : NfExpr N₁ N₂) → + ⌊ f ∘ⁿ g ⌋ ≈↓ ⌊ f ⌋ ∘′ ⌊ g ⌋ + ⌊⌋-∘ id′ id′ = ⟺ identity² + + ⌞⌟-⊗ : ∀ N M → Expr (⌞ N ⌟ ⊗₀′ ⌞ M ⌟) ⌞ N ++ M ⌟ + ⌞⌟-⊗ [] M = ƛ′ + ⌞⌟-⊗ (X ∷ N) M = id′ ⊗₁′ ⌞⌟-⊗ N M ∘′ α′ + + ⌊⌋-⊗ : ∀ {N₁ N₂ M₁ M₂} (f : NfExpr N₁ M₁) (g : NfExpr N₂ M₂) → + ⌊ f ⊗ⁿ g ⌋ ∘′ ⌞⌟-⊗ N₁ N₂ ≈↓ ⌞⌟-⊗ M₁ M₂ ∘′ ⌊ f ⌋ ⊗₁′ ⌊ g ⌋ + ⌊⌋-⊗ {N₁} {N₂} id′ id′ = begin + id ∘ [ ⌞⌟-⊗ N₁ N₂ ↓] ≈⟨ id-comm-sym ⟩ + [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ id ≈˘⟨ refl⟩∘⟨ ⊗.identity ⟩ + [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ id ⊗₁ id ∎ + + ⌊⌋-ρ : ∀ N → ⌊ ρⁿ N ⌋ ∘′ ⌞⌟-⊗ N [] ≈↓ ρ′ + ⌊⌋-ρ [] = identityˡ ○ Kelly's.coherence₃ 𝒱 + ⌊⌋-ρ (X ∷ N) = begin + [ ⌊ subst (NfExpr (X ∷ N ++ [])) (cong (X ∷_) (++-identityʳ N)) id′ ⌋ ↓] ∘ + id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from + ≡⟨ cong (λ f → [ ⌊ f ⌋ ∘′ id′ ⊗₁′ ⌞⌟-⊗ N [] ∘′ α′ ↓]) + (helper₁ (++-identityʳ N)) ⟩ + [ ⌊ id′ ⊗ⁿ ρⁿ N ⌋ ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from + ≈⟨ helper₂ (ρⁿ N) ⟩∘⟨refl ⟩ + id ⊗₁ [ ⌊ ρⁿ N ⌋ ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from + ≈⟨ merge₂ ⌊⌋-ρ N ⟩∘⟨ Equiv.refl ⟩ + id ⊗₁ unitorʳ.from ∘ associator.from + ≈⟨ Kelly's.coherence₂ 𝒱 ⟩ + unitorʳ.from + ∎ + where + + -- FIXME: give these better names and reuse them in the proof of + -- the hexagon identity (the ⌊⌋-α yet to be written). + + helper₁ : ∀ {X N M} (eq : N ≡ M) → + subst (NfExpr (X ∷ N)) (cong (X ∷_) eq) (id′ ⊗ⁿ id′ {N}) ≡ + id′ ⊗ⁿ subst (NfExpr N) eq id′ + helper₁ refl = refl + + helper₂ : ∀ {X N M} (f : NfExpr N M) → ⌊ id′ ⊗ⁿ f ⌋ ≈↓ id′ {X ′} ⊗₁′ ⌊ f ⌋ + helper₂ id′ = ⟺ ⊗.identity + + -- Build a coherence morphism out of some word into it's normal form. + into : ∀ (A : Word) → Expr A ⌞ nf₀ A ⌟ + into (A ⊗₀′ B) = ⌞⌟-⊗ (nf₀ A) (nf₀ B) ∘′ (into A ⊗₁′ into B) + into unit′ = id′ + into (x ′) = ρ⁻¹′ + + -- Build a coherence morphism into a word from it's normal form. + out : ∀ (A : Word) → Expr ⌞ nf₀ A ⌟ A + out A = invert (into A) + + -- Normalize an expression. + -- We do this by building maps into and out of the normal forms of the + -- domain/codomain, then using our 'strict' coherence morphism to link them together. + normalize : Expr A B → Expr A B + normalize {A = A} {B = B} f = out B ∘′ ⌊ nf₁ f ⌋ ∘′ into A + + -- Witness the isomorphism between 'f' and 'invert f'. + invert-isoˡ : ∀ (f : Expr A B) → [ invert f ↓] ∘ [ f ↓] ≈ id + invert-isoˡ id′ = identity² + invert-isoˡ (f ∘′ g) = begin + ([ invert g ↓] ∘ [ invert f ↓]) ∘ ([ f ↓] ∘ [ g ↓]) ≈⟨ cancelInner (invert-isoˡ f) ⟩ + [ invert g ↓] ∘ [ g ↓] ≈⟨ invert-isoˡ g ⟩ + id ∎ + invert-isoˡ (f ⊗₁′ g) = begin + ([ invert f ↓] ⊗₁ [ invert g ↓]) ∘ ([ f ↓] ⊗₁ [ g ↓]) ≈˘⟨ ⊗.homomorphism ⟩ + ([ invert f ↓] ∘ [ f ↓]) ⊗₁ ([ invert g ↓] ∘ [ g ↓]) ≈⟨ ⊗.F-resp-≈ (invert-isoˡ f , invert-isoˡ g) ⟩ + id ⊗₁ id ≈⟨ ⊗.identity ⟩ + id ∎ + invert-isoˡ α′ = associator.isoˡ + invert-isoˡ α⁻¹′ = associator.isoʳ + invert-isoˡ ƛ′ = unitorˡ.isoˡ + invert-isoˡ ƛ⁻¹′ = unitorˡ.isoʳ + invert-isoˡ ρ′ = unitorʳ.isoˡ + invert-isoˡ ρ⁻¹′ = unitorʳ.isoʳ + + -- Witness the isomorphism between 'f' and 'invert f'. + invert-isoʳ : ∀ (f : Expr A B) → [ f ↓] ∘ [ invert f ↓] ≈ id + invert-isoʳ id′ = identity² + invert-isoʳ (f ∘′ g) = begin + ([ f ↓] ∘ [ g ↓]) ∘ ([ invert g ↓] ∘ [ invert f ↓]) ≈⟨ cancelInner (invert-isoʳ g) ⟩ + [ f ↓] ∘ [ invert f ↓] ≈⟨ invert-isoʳ f ⟩ + id ∎ + invert-isoʳ (f ⊗₁′ g) = begin + ([ f ↓] ⊗₁ [ g ↓]) ∘ ([ invert f ↓] ⊗₁ [ invert g ↓]) ≈˘⟨ ⊗.homomorphism ⟩ + ([ f ↓] ∘ [ invert f ↓]) ⊗₁ ([ g ↓] ∘ [ invert g ↓]) ≈⟨ ⊗.F-resp-≈ (invert-isoʳ f , invert-isoʳ g) ⟩ + id ⊗₁ id ≈⟨ ⊗.identity ⟩ + id ∎ + invert-isoʳ α′ = associator.isoʳ + invert-isoʳ α⁻¹′ = associator.isoˡ + invert-isoʳ ƛ′ = unitorˡ.isoʳ + invert-isoʳ ƛ⁻¹′ = unitorˡ.isoˡ + invert-isoʳ ρ′ = unitorʳ.isoʳ + invert-isoʳ ρ⁻¹′ = unitorʳ.isoˡ + + -- Helper lemma for showing that mapping into a normal form then back out + -- is identity. + into-out : ∀ (A : Word) → [ out A ↓] ∘ id ∘ [ into A ↓] ≈ id + into-out A = begin + [ out A ↓] ∘ id ∘ [ into A ↓] ≈⟨ refl⟩∘⟨ identityˡ ⟩ + [ out A ↓] ∘ [ into A ↓] ≈⟨ invert-isoˡ (into A) ⟩ + id ∎ + + -- Normalization preserves equality. + preserves-≈ : ∀ (f : Expr A B) → normalize f ≈↓ f + preserves-≈ (id′ {A}) = into-out A + preserves-≈ (_∘′_ {B} {C} {A} f g) = begin + [ out C ↓] ∘ [ ⌊ nf₁ (f ∘′ g) ⌋ ↓] ∘ [ into A ↓] + ≈⟨ refl⟩∘⟨ ⌊⌋-∘ (nf₁ f) (nf₁ g) ⟩∘⟨refl ⟩ + [ out C ↓] ∘ ([ ⌊ nf₁ f ⌋ ↓] ∘ [ ⌊ nf₁ g ⌋ ↓]) ∘ [ into A ↓] + ≈˘⟨ refl⟩∘⟨ cancelInner (invert-isoʳ (into B)) ⟩∘⟨refl ⟩ + [ out C ↓] ∘ + (([ ⌊ nf₁ f ⌋ ↓] ∘ [ into B ↓]) ∘ ([ out B ↓] ∘ [ ⌊ nf₁ g ⌋ ↓])) ∘ + [ into A ↓] + ≈⟨ center⁻¹ (preserves-≈ f) (assoc ○ preserves-≈ g) ⟩ + [ f ↓] ∘ [ g ↓] + ∎ + preserves-≈ (_⊗₁′_ {A} {C} {B} {D} f g) = begin + ([ out C ↓] ⊗₁ [ out D ↓] ∘ [ invert (⌞⌟-⊗ (nf₀ C) (nf₀ D)) ↓]) ∘ + [ ⌊ nf₁ (f ⊗₁′ g) ⌋ ↓] ∘ + [ ⌞⌟-⊗ (nf₀ A) (nf₀ B) ↓] ∘ [ into A ↓] ⊗₁ [ into B ↓] + ≈⟨ (refl⟩∘⟨ pullˡ (⌊⌋-⊗ (nf₁ f) (nf₁ g))) ⟩ + ([ out C ↓] ⊗₁ [ out D ↓] ∘ [ invert (⌞⌟-⊗ (nf₀ C) (nf₀ D)) ↓]) ∘ + ([ ⌞⌟-⊗ (nf₀ C) (nf₀ D) ↓] ∘ [ ⌊ nf₁ f ⌋ ⊗₁′ ⌊ nf₁ g ⌋ ↓]) ∘ + [ into A ↓] ⊗₁ [ into B ↓] + ≈⟨ pullˡ (cancelInner (invert-isoˡ (⌞⌟-⊗ (nf₀ C) (nf₀ D)))) ⟩ + ([ out C ⊗₁′ out D ↓] ∘ [ ⌊ nf₁ f ⌋ ⊗₁′ ⌊ nf₁ g ⌋ ↓]) ∘ + [ into A ⊗₁′ into B ↓] + ≈˘⟨ pushʳ ⊗.homomorphism ⟩ + ([ out C ⊗₁′ out D ↓] ∘ [ (⌊ nf₁ f ⌋ ∘′ into A) ⊗₁′ (⌊ nf₁ g ⌋ ∘′ into B) ↓]) + ≈˘⟨ ⊗.homomorphism ⟩ + ([ out C ∘′ ⌊ nf₁ f ⌋ ∘′ into A ↓] ⊗₁ [ out D ∘′ ⌊ nf₁ g ⌋ ∘′ into B ↓]) + ≈⟨ preserves-≈ f ⟩⊗⟨ preserves-≈ g ⟩ + [ f ↓] ⊗₁ [ g ↓] + ∎ + preserves-≈ (α′ {A} {B} {C}) = {!!} + preserves-≈ α⁻¹′ = {!!} + preserves-≈ (ƛ′ {A}) = begin + [ out A ↓] ∘ id ∘ unitorˡ.from ∘ id ⊗₁ [ into A ↓] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-from ⟩ + [ out A ↓] ∘ id ∘ [ into A ↓] ∘ unitorˡ.from ≈˘⟨ assoc²' ⟩ + ([ out A ↓] ∘ id ∘ [ into A ↓]) ∘ unitorˡ.from ≈⟨ elimˡ (into-out A) ⟩ + unitorˡ.from ∎ + preserves-≈ (ƛ⁻¹′ {A}) = begin + (id ⊗₁ [ out A ↓] ∘ unitorˡ.to) ∘ id ∘ [ into A ↓] ≈˘⟨ unitorˡ-commute-to ⟩∘⟨refl ⟩ + (unitorˡ.to ∘ [ out A ↓]) ∘ id ∘ [ into A ↓] ≈⟨ cancelʳ (into-out A) ⟩ + unitorˡ.to ∎ + preserves-≈ (ρ′ {A}) = begin + [ out A ↓] ∘ [ ⌊ ρⁿ (nf₀ A) ⌋ ↓] ∘ [ ⌞⌟-⊗ (nf₀ A) [] ↓] ∘ [ into A ↓] ⊗₁ id + ≈⟨ refl⟩∘⟨ pullˡ (⌊⌋-ρ (nf₀ A)) ⟩ + [ out A ↓] ∘ unitorʳ.from ∘ ([ into A ↓] ⊗₁ id) + ≈⟨ refl⟩∘⟨ unitorʳ-commute-from ⟩ + [ out A ↓] ∘ [ into A ↓] ∘ unitorʳ.from + ≈⟨ cancelˡ (invert-isoˡ (into A)) ⟩ + unitorʳ.from + ∎ + preserves-≈ (ρ⁻¹′ {A}) = {!!} From e36b0129823b7dab4954439ed93680b11f74b71a Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Tue, 4 May 2021 18:31:27 -0700 Subject: [PATCH 3/7] =?UTF-8?q?Prove=20the=20=CF=81=E2=81=BB=C2=B9?= =?UTF-8?q?=E2=80=B2=20case?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Categories/Tactic/Monoidal.agda | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/src/Categories/Tactic/Monoidal.agda b/src/Categories/Tactic/Monoidal.agda index af2e8ff95..cfeceb795 100644 --- a/src/Categories/Tactic/Monoidal.agda +++ b/src/Categories/Tactic/Monoidal.agda @@ -210,6 +210,15 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where helper₂ : ∀ {X N M} (f : NfExpr N M) → ⌊ id′ ⊗ⁿ f ⌋ ≈↓ id′ {X ′} ⊗₁′ ⌊ f ⌋ helper₂ id′ = ⟺ ⊗.identity + invert-resp-≈ : ∀ (f g : Expr A B) → f ≈↓ g → invert f ≈↓ invert g + invert-resp-≈ f g eq = {!!} + + ⌊⌋-invert : ∀ {M} {N O} (f : Expr M ⌞ N ⌟) (g : NfExpr N O) (h : Expr M ⌞ O ⌟) → ⌊ g ⌋ ∘′ f ≈↓ h → invert f ∘′ ⌊ invertⁿ g ⌋ ≈↓ invert h + ⌊⌋-invert f id′ h eq = begin + [ invert f ↓] ∘ id ≈⟨ identityʳ ⟩ + [ invert f ↓] ≈⟨ invert-resp-≈ f h (⟺ identityˡ ○ eq) ⟩ + [ invert h ↓] ∎ + -- Build a coherence morphism out of some word into it's normal form. into : ∀ (A : Word) → Expr A ⌞ nf₀ A ⌟ into (A ⊗₀′ B) = ⌞⌟-⊗ (nf₀ A) (nf₀ B) ∘′ (into A ⊗₁′ into B) @@ -324,4 +333,15 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ≈⟨ cancelˡ (invert-isoˡ (into A)) ⟩ unitorʳ.from ∎ - preserves-≈ (ρ⁻¹′ {A}) = {!!} + preserves-≈ (ρ⁻¹′ {A}) = begin + ([ out A ↓] ⊗₁ id ∘ [ invert (⌞⌟-⊗ (nf₀ A) []) ↓]) ∘ ([ ⌊ invertⁿ (ρⁿ (nf₀ A)) ⌋ ↓] ∘ [ into A ↓]) + ≈⟨ center (⌊⌋-invert (⌞⌟-⊗ (nf₀ A) []) (ρⁿ (nf₀ A)) ρ′ (⌊⌋-ρ (nf₀ A))) ⟩ + [ out A ↓] ⊗₁ id ∘ unitorʳ.to ∘ [ into A ↓] + ≈⟨ refl⟩∘⟨ unitorʳ-commute-to ⟩ + [ out A ↓] ⊗₁ id ∘ [ into A ↓] ⊗₁ id ∘ unitorʳ.to + ≈⟨ pullˡ (⟺ ⊗.homomorphism) ⟩ + ([ out A ↓] ∘ [ into A ↓]) ⊗₁ (id ∘ id) ∘ unitorʳ.to + ≈⟨ (invert-isoˡ (into A) ⟩⊗⟨ identity²) ⟩∘⟨refl ⟩ + id ⊗₁ id ∘ unitorʳ.to + ≈⟨ elimˡ ⊗.identity ⟩ + unitorʳ.to ∎ From 60ad8f50eb5d2b077b391a9efbcb717ba0ecb1da Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Wed, 5 May 2021 13:24:36 -0700 Subject: [PATCH 4/7] =?UTF-8?q?Add=20a=20=E2=8A=97-elim=20to=20Monoidal=20?= =?UTF-8?q?Reasoning?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Categories/Category/Monoidal/Reasoning.agda | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Categories/Category/Monoidal/Reasoning.agda b/src/Categories/Category/Monoidal/Reasoning.agda index cc66a819c..d1b877fc0 100644 --- a/src/Categories/Category/Monoidal/Reasoning.agda +++ b/src/Categories/Category/Monoidal/Reasoning.agda @@ -134,6 +134,13 @@ split₂ˡ {f = f} {g} {h} = begin (id ∘ f) ⊗₁ (g ∘ h) ≈⟨ ⊗-distrib-over-∘ ⟩ id ⊗₁ g ∘ f ⊗₁ h ∎ +⊗-elim : ∀ {X₁ Y₁ X₂ Y₂} {f : Y₁ ⇒ X₁} {g : X₁ ⇒ Y₁} {h : Y₂ ⇒ X₂} {i : X₂ ⇒ Y₂} → f ∘ g ≈ id → h ∘ i ≈ id → f ⊗₁ h ∘ g ⊗₁ i ≈ id +⊗-elim {f = f} {g = g} {h = h} {i = i} f∘g≈id h∘i≈id = begin + f ⊗₁ h ∘ g ⊗₁ i ≈˘⟨ ⊗-distrib-over-∘ ⟩ + (f ∘ g) ⊗₁ (h ∘ i) ≈⟨ f∘g≈id ⟩⊗⟨ h∘i≈id ⟩ + id ⊗₁ id ≈⟨ ⊗.identity ⟩ + id ∎ + -- Combined splitting and re-association. module _ {X Y Z} {f : X ⇒ Z} {g : Y ⇒ Z} {h : X ⇒ Y} (f≈gh : f ≈ g ∘ h) where From e894e16dae23e4189d2ab573582ea3c19306b526 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Wed, 5 May 2021 13:25:10 -0700 Subject: [PATCH 5/7] Work on the associator case --- src/Categories/Tactic/Monoidal.agda | 206 +++++++++++++++++++--------- 1 file changed, 139 insertions(+), 67 deletions(-) diff --git a/src/Categories/Tactic/Monoidal.agda b/src/Categories/Tactic/Monoidal.agda index cfeceb795..fe859808d 100644 --- a/src/Categories/Tactic/Monoidal.agda +++ b/src/Categories/Tactic/Monoidal.agda @@ -19,6 +19,8 @@ open import Categories.Category.Monoidal.Core using (Monoidal) import Categories.Category.Monoidal.Reasoning as MonoidalReasoning open import Categories.Category.Monoidal.Properties using (module Kelly's) +import Categories.Morphism as Mor +import Categories.Morphism.IsoEquiv as Iso import Categories.Morphism.Reasoning as MR -------------------------------------------------------------------------------- @@ -39,6 +41,8 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where open Category 𝒞 open Monoidal 𝒱 + open Iso 𝒞 using (to-unique) + open Mor 𝒞 open MR 𝒞 open MonoidalReasoning 𝒱 @@ -107,11 +111,50 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where invert ρ′ = ρ⁻¹′ invert ρ⁻¹′ = ρ′ + -- Witness the isomorphism between 'f' and 'invert f'. + invert-isoˡ : ∀ (f : Expr A B) → [ invert f ↓] ∘ [ f ↓] ≈ id + invert-isoˡ id′ = identity² + invert-isoˡ (f ∘′ g) = begin + ([ invert g ↓] ∘ [ invert f ↓]) ∘ ([ f ↓] ∘ [ g ↓]) ≈⟨ cancelInner (invert-isoˡ f) ⟩ + [ invert g ↓] ∘ [ g ↓] ≈⟨ invert-isoˡ g ⟩ + id ∎ + invert-isoˡ (f ⊗₁′ g) = begin + ([ invert f ↓] ⊗₁ [ invert g ↓]) ∘ ([ f ↓] ⊗₁ [ g ↓]) ≈⟨ ⊗-elim (invert-isoˡ f) (invert-isoˡ g) ⟩ + id ∎ + invert-isoˡ α′ = associator.isoˡ + invert-isoˡ α⁻¹′ = associator.isoʳ + invert-isoˡ ƛ′ = unitorˡ.isoˡ + invert-isoˡ ƛ⁻¹′ = unitorˡ.isoʳ + invert-isoˡ ρ′ = unitorʳ.isoˡ + invert-isoˡ ρ⁻¹′ = unitorʳ.isoʳ + + invert-isoʳ : ∀ (f : Expr A B) → [ f ↓] ∘ [ invert f ↓] ≈ id + invert-isoʳ id′ = identity² + invert-isoʳ (f ∘′ g) = begin + ([ f ↓] ∘ [ g ↓]) ∘ ([ invert g ↓] ∘ [ invert f ↓]) ≈⟨ cancelInner (invert-isoʳ g) ⟩ + [ f ↓] ∘ [ invert f ↓] ≈⟨ invert-isoʳ f ⟩ + id ∎ + invert-isoʳ (f ⊗₁′ g) = begin + ([ f ↓] ⊗₁ [ g ↓]) ∘ ([ invert f ↓] ⊗₁ [ invert g ↓]) ≈⟨ ⊗-elim (invert-isoʳ f) (invert-isoʳ g) ⟩ + id ∎ + invert-isoʳ α′ = associator.isoʳ + invert-isoʳ α⁻¹′ = associator.isoˡ + invert-isoʳ ƛ′ = unitorˡ.isoʳ + invert-isoʳ ƛ⁻¹′ = unitorˡ.isoˡ + invert-isoʳ ρ′ = unitorʳ.isoʳ + invert-isoʳ ρ⁻¹′ = unitorʳ.isoˡ + + invert-iso : ∀ (f : Expr A B) → Iso [ f ↓] [ invert f ↓] + invert-iso f = record + { isoˡ = invert-isoˡ f + ; isoʳ = invert-isoʳ f + } + NfWord : Set o NfWord = List Obj data NfExpr : NfWord → NfWord → Set o where - id′ : ∀ {N} → NfExpr N N + idⁿ : ∀ {N} → NfExpr N N -- An embedding of normal forms @@ -120,7 +163,7 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ⌞ A ∷ N ⌟ = (A ′) ⊗₀′ ⌞ N ⌟ ⌊_⌋ : ∀ {N M} → NfExpr N M → Expr ⌞ N ⌟ ⌞ M ⌟ - ⌊ id′ ⌋ = id′ + ⌊ idⁿ ⌋ = id′ -- The monoidal operations are all admissible on normal forms. @@ -129,20 +172,20 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where _∘ⁿ_ : ∀ {N₁ N₂ N₃} → NfExpr N₂ N₃ → NfExpr N₁ N₂ → NfExpr N₁ N₃ - id′ ∘ⁿ id′ = id′ + idⁿ ∘ⁿ idⁿ = idⁿ _⊗ⁿ_ : ∀ {N₁ N₂ M₁ M₂} → NfExpr N₁ M₁ → NfExpr N₂ M₂ → NfExpr (N₁ ++ N₂) (M₁ ++ M₂) - id′ ⊗ⁿ id′ = id′ + idⁿ ⊗ⁿ idⁿ = idⁿ αⁿ : ∀ N₁ N₂ N₃ → NfExpr ((N₁ ++ N₂) ++ N₃) (N₁ ++ (N₂ ++ N₃)) - αⁿ N₁ N₂ N₃ = subst (NfExpr ((N₁ ++ N₂) ++ N₃)) (++-assoc N₁ N₂ N₃) id′ + αⁿ N₁ N₂ N₃ = subst (NfExpr ((N₁ ++ N₂) ++ N₃)) (++-assoc N₁ N₂ N₃) idⁿ ρⁿ : ∀ N → NfExpr (N ++ []) N - ρⁿ N = subst (NfExpr (N ++ [])) (++-identityʳ N) id′ + ρⁿ N = subst (NfExpr (N ++ [])) (++-identityʳ N) idⁿ invertⁿ : ∀ {N M} → NfExpr N M → NfExpr M N - invertⁿ id′ = id′ + invertⁿ idⁿ = idⁿ -- The normalization functor @@ -152,24 +195,24 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where nf₀ (X ′) = X ∷ [] nf₁ : Expr A B → NfExpr (nf₀ A) (nf₀ B) - nf₁ id′ = id′ + nf₁ id′ = idⁿ nf₁ (f ∘′ g) = nf₁ f ∘ⁿ nf₁ g nf₁ (f ⊗₁′ g) = nf₁ f ⊗ⁿ nf₁ g nf₁ (α′ {A} {B} {C}) = αⁿ (nf₀ A) (nf₀ B) (nf₀ C) nf₁ (α⁻¹′ {A} {B} {C}) = invertⁿ (αⁿ (nf₀ A) (nf₀ B) (nf₀ C)) - nf₁ ƛ′ = id′ - nf₁ ƛ⁻¹′ = id′ + nf₁ ƛ′ = idⁿ + nf₁ ƛ⁻¹′ = idⁿ nf₁ ρ′ = ρⁿ _ nf₁ ρ⁻¹′ = invertⁿ (ρⁿ _) -- The embedding is a monoidal functor - ⌊⌋-id : ∀ {N} → ⌊ id′ {N} ⌋ ≈↓ id′ + ⌊⌋-id : ∀ {N} → ⌊ idⁿ {N} ⌋ ≈↓ id′ ⌊⌋-id = Equiv.refl ⌊⌋-∘ : ∀ {N₁ N₂ N₃} (f : NfExpr N₂ N₃) (g : NfExpr N₁ N₂) → ⌊ f ∘ⁿ g ⌋ ≈↓ ⌊ f ⌋ ∘′ ⌊ g ⌋ - ⌊⌋-∘ id′ id′ = ⟺ identity² + ⌊⌋-∘ idⁿ idⁿ = ⟺ identity² ⌞⌟-⊗ : ∀ N M → Expr (⌞ N ⌟ ⊗₀′ ⌞ M ⌟) ⌞ N ++ M ⌟ ⌞⌟-⊗ [] M = ƛ′ @@ -177,7 +220,7 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ⌊⌋-⊗ : ∀ {N₁ N₂ M₁ M₂} (f : NfExpr N₁ M₁) (g : NfExpr N₂ M₂) → ⌊ f ⊗ⁿ g ⌋ ∘′ ⌞⌟-⊗ N₁ N₂ ≈↓ ⌞⌟-⊗ M₁ M₂ ∘′ ⌊ f ⌋ ⊗₁′ ⌊ g ⌋ - ⌊⌋-⊗ {N₁} {N₂} id′ id′ = begin + ⌊⌋-⊗ {N₁} {N₂} idⁿ idⁿ = begin id ∘ [ ⌞⌟-⊗ N₁ N₂ ↓] ≈⟨ id-comm-sym ⟩ [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ id ≈˘⟨ refl⟩∘⟨ ⊗.identity ⟩ [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ id ⊗₁ id ∎ @@ -185,11 +228,11 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ⌊⌋-ρ : ∀ N → ⌊ ρⁿ N ⌋ ∘′ ⌞⌟-⊗ N [] ≈↓ ρ′ ⌊⌋-ρ [] = identityˡ ○ Kelly's.coherence₃ 𝒱 ⌊⌋-ρ (X ∷ N) = begin - [ ⌊ subst (NfExpr (X ∷ N ++ [])) (cong (X ∷_) (++-identityʳ N)) id′ ⌋ ↓] ∘ + [ ⌊ subst (NfExpr (X ∷ N ++ [])) (cong (X ∷_) (++-identityʳ N)) idⁿ ⌋ ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from ≡⟨ cong (λ f → [ ⌊ f ⌋ ∘′ id′ ⊗₁′ ⌞⌟-⊗ N [] ∘′ α′ ↓]) (helper₁ (++-identityʳ N)) ⟩ - [ ⌊ id′ ⊗ⁿ ρⁿ N ⌋ ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from + [ ⌊ idⁿ ⊗ⁿ ρⁿ N ⌋ ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from ≈⟨ helper₂ (ρⁿ N) ⟩∘⟨refl ⟩ id ⊗₁ [ ⌊ ρⁿ N ⌋ ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from ≈⟨ merge₂ ⌊⌋-ρ N ⟩∘⟨ Equiv.refl ⟩ @@ -203,20 +246,69 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where -- the hexagon identity (the ⌊⌋-α yet to be written). helper₁ : ∀ {X N M} (eq : N ≡ M) → - subst (NfExpr (X ∷ N)) (cong (X ∷_) eq) (id′ ⊗ⁿ id′ {N}) ≡ - id′ ⊗ⁿ subst (NfExpr N) eq id′ + subst (NfExpr (X ∷ N)) (cong (X ∷_) eq) (idⁿ ⊗ⁿ idⁿ {N}) ≡ + idⁿ ⊗ⁿ subst (NfExpr N) eq idⁿ helper₁ refl = refl - helper₂ : ∀ {X N M} (f : NfExpr N M) → ⌊ id′ ⊗ⁿ f ⌋ ≈↓ id′ {X ′} ⊗₁′ ⌊ f ⌋ - helper₂ id′ = ⟺ ⊗.identity + helper₂ : ∀ {X N M} (f : NfExpr N M) → ⌊ idⁿ ⊗ⁿ f ⌋ ≈↓ id′ {X ′} ⊗₁′ ⌊ f ⌋ + helper₂ idⁿ = ⟺ ⊗.identity + + ⌊⌋-α : ∀ N₁ N₂ N₃ → ⌊ αⁿ N₁ N₂ N₃ ⌋ ∘′ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ∘′ ⌞⌟-⊗ N₁ N₂ ⊗₁′ id′ ≈↓ ⌞⌟-⊗ N₁ (N₂ ++ N₃) ∘′ id′ ⊗₁′ (⌞⌟-⊗ N₂ N₃) ∘′ α′ + ⌊⌋-α [] N₂ N₃ = begin + id ∘ [ ⌞⌟-⊗ N₂ N₃ ↓] ∘ (unitorˡ.from ⊗₁ id) ≈⟨ identityˡ ⟩ + [ ⌞⌟-⊗ N₂ N₃ ↓] ∘ (unitorˡ.from ⊗₁ id) ≈⟨ refl⟩∘⟨ (⟺ (Kelly's.coherence₁ 𝒱)) ⟩ + [ ⌞⌟-⊗ N₂ N₃ ↓] ∘ (unitorˡ.from ∘ associator.from) ≈⟨ extendʳ (⟺ unitorˡ-commute-from) ⟩ + unitorˡ.from ∘ (id ⊗₁ [ ⌞⌟-⊗ N₂ N₃ ↓]) ∘ associator.from ∎ + ⌊⌋-α (X ∷ N₁) N₂ N₃ = begin + [ ⌊ subst (NfExpr (X ∷ (N₁ ++ N₂) ++ N₃)) (cong (_∷_ X) (++-assoc N₁ N₂ N₃)) idⁿ ⌋ ↓] ∘ + (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ (id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ associator.from) ⊗₁ id + ≡⟨ cong (λ f → [ ⌊ f ⌋ ↓] ∘ (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ (id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ associator.from) ⊗₁ id) (helper₁ (++-assoc N₁ N₂ N₃)) ⟩ + [ ⌊ idⁿ ⊗ⁿ subst (NfExpr ((N₁ ++ N₂) ++ N₃)) (++-assoc N₁ N₂ N₃) idⁿ ⌋ ↓] ∘ + (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ + (id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ associator.from) ⊗₁ id + ≈⟨ helper₂ (subst (NfExpr ((N₁ ++ N₂) ++ N₃)) (++-assoc N₁ N₂ N₃) idⁿ) ⟩∘⟨refl ⟩ + (id ⊗₁ [ ⌊ αⁿ N₁ N₂ N₃ ⌋ ↓]) ∘ + (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ + ((id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓]) ∘ associator.from) ⊗₁ id + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ʳ ⟩ + (id ⊗₁ [ ⌊ αⁿ N₁ N₂ N₃ ⌋ ↓]) ∘ + (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ + (id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓]) ⊗₁ id ∘ (associator.from ⊗₁ id) + ≈⟨ center⁻¹ (⟺ ⊗.homomorphism ○ identity² ⟩⊗⟨refl) (extendʳ assoc-commute-from) ⟩ + id ⊗₁ ([ ⌊ αⁿ N₁ N₂ N₃ ⌋ ↓] ∘ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓]) ∘ + (id ⊗₁ ([ ⌞⌟-⊗ N₁ N₂ ↓] ⊗₁ id)) ∘ associator.from ∘ + associator.from ⊗₁ id + ≈⟨ merge₂ assoc ○ ⌊⌋-α N₁ N₂ N₃ ⟩∘⟨ Equiv.refl ⟩ + id ⊗₁ ([ ⌞⌟-⊗ N₁ (N₂ ++ N₃) ↓] ∘ (id ⊗₁ ([ ⌞⌟-⊗ N₂ N₃ ↓]) ∘ associator.from)) ∘ + associator.from ∘ (associator.from ⊗₁ id) + ≈⟨ (pushˡ (split₂ʳ ○ (refl⟩∘⟨ split₂ʳ))) ⟩ + id ⊗₁ [ ⌞⌟-⊗ N₁ (N₂ ++ N₃) ↓] ∘ (id ⊗₁ (id ⊗₁ [ ⌞⌟-⊗ N₂ N₃ ↓]) ∘ id ⊗₁ associator.from) ∘ + associator.from ∘ (associator.from ⊗₁ id) + ≈⟨ refl⟩∘⟨ pullʳ pentagon ⟩ + id ⊗₁ [ ⌞⌟-⊗ N₁ (N₂ ++ N₃) ↓] ∘ id ⊗₁ (id ⊗₁ [ ⌞⌟-⊗ N₂ N₃ ↓]) ∘ associator.from ∘ associator.from + ≈⟨ pushʳ (extendʳ (⟺ assoc-commute-from)) ⟩ + (id ⊗₁ [ ⌞⌟-⊗ N₁ (N₂ ++ N₃) ↓] ∘ associator.from) ∘ + ((id ⊗₁ id) ⊗₁ [ ⌞⌟-⊗ N₂ N₃ ↓] ∘ associator.from) + ≈⟨ (refl⟩∘⟨ (⊗.identity ⟩⊗⟨refl) ⟩∘⟨refl) ⟩ + (id ⊗₁ [ ⌞⌟-⊗ N₁ (N₂ ++ N₃) ↓] ∘ associator.from) ∘ + (id ⊗₁ [ ⌞⌟-⊗ N₂ N₃ ↓] ∘ associator.from) ∎ + where + + -- FIXME: give these better names and reuse them in the proof of + -- the hexagon identity (the ⌊⌋-α yet to be written). + + helper₁ : ∀ {X N M} (eq : N ≡ M) → + subst (NfExpr (X ∷ N)) (cong (X ∷_) eq) (idⁿ ⊗ⁿ idⁿ {N}) ≡ + idⁿ ⊗ⁿ subst (NfExpr N) eq idⁿ + helper₁ refl = refl - invert-resp-≈ : ∀ (f g : Expr A B) → f ≈↓ g → invert f ≈↓ invert g - invert-resp-≈ f g eq = {!!} + helper₂ : ∀ {X N M} (f : NfExpr N M) → ⌊ idⁿ ⊗ⁿ f ⌋ ≈↓ id′ {X ′} ⊗₁′ ⌊ f ⌋ + helper₂ idⁿ = ⟺ ⊗.identity ⌊⌋-invert : ∀ {M} {N O} (f : Expr M ⌞ N ⌟) (g : NfExpr N O) (h : Expr M ⌞ O ⌟) → ⌊ g ⌋ ∘′ f ≈↓ h → invert f ∘′ ⌊ invertⁿ g ⌋ ≈↓ invert h - ⌊⌋-invert f id′ h eq = begin + ⌊⌋-invert f idⁿ h eq = begin [ invert f ↓] ∘ id ≈⟨ identityʳ ⟩ - [ invert f ↓] ≈⟨ invert-resp-≈ f h (⟺ identityˡ ○ eq) ⟩ + [ invert f ↓] ≈⟨ to-unique (invert-iso f) (invert-iso h) (⟺ identityˡ ○ eq) ⟩ [ invert h ↓] ∎ -- Build a coherence morphism out of some word into it's normal form. @@ -235,43 +327,6 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where normalize : Expr A B → Expr A B normalize {A = A} {B = B} f = out B ∘′ ⌊ nf₁ f ⌋ ∘′ into A - -- Witness the isomorphism between 'f' and 'invert f'. - invert-isoˡ : ∀ (f : Expr A B) → [ invert f ↓] ∘ [ f ↓] ≈ id - invert-isoˡ id′ = identity² - invert-isoˡ (f ∘′ g) = begin - ([ invert g ↓] ∘ [ invert f ↓]) ∘ ([ f ↓] ∘ [ g ↓]) ≈⟨ cancelInner (invert-isoˡ f) ⟩ - [ invert g ↓] ∘ [ g ↓] ≈⟨ invert-isoˡ g ⟩ - id ∎ - invert-isoˡ (f ⊗₁′ g) = begin - ([ invert f ↓] ⊗₁ [ invert g ↓]) ∘ ([ f ↓] ⊗₁ [ g ↓]) ≈˘⟨ ⊗.homomorphism ⟩ - ([ invert f ↓] ∘ [ f ↓]) ⊗₁ ([ invert g ↓] ∘ [ g ↓]) ≈⟨ ⊗.F-resp-≈ (invert-isoˡ f , invert-isoˡ g) ⟩ - id ⊗₁ id ≈⟨ ⊗.identity ⟩ - id ∎ - invert-isoˡ α′ = associator.isoˡ - invert-isoˡ α⁻¹′ = associator.isoʳ - invert-isoˡ ƛ′ = unitorˡ.isoˡ - invert-isoˡ ƛ⁻¹′ = unitorˡ.isoʳ - invert-isoˡ ρ′ = unitorʳ.isoˡ - invert-isoˡ ρ⁻¹′ = unitorʳ.isoʳ - - -- Witness the isomorphism between 'f' and 'invert f'. - invert-isoʳ : ∀ (f : Expr A B) → [ f ↓] ∘ [ invert f ↓] ≈ id - invert-isoʳ id′ = identity² - invert-isoʳ (f ∘′ g) = begin - ([ f ↓] ∘ [ g ↓]) ∘ ([ invert g ↓] ∘ [ invert f ↓]) ≈⟨ cancelInner (invert-isoʳ g) ⟩ - [ f ↓] ∘ [ invert f ↓] ≈⟨ invert-isoʳ f ⟩ - id ∎ - invert-isoʳ (f ⊗₁′ g) = begin - ([ f ↓] ⊗₁ [ g ↓]) ∘ ([ invert f ↓] ⊗₁ [ invert g ↓]) ≈˘⟨ ⊗.homomorphism ⟩ - ([ f ↓] ∘ [ invert f ↓]) ⊗₁ ([ g ↓] ∘ [ invert g ↓]) ≈⟨ ⊗.F-resp-≈ (invert-isoʳ f , invert-isoʳ g) ⟩ - id ⊗₁ id ≈⟨ ⊗.identity ⟩ - id ∎ - invert-isoʳ α′ = associator.isoʳ - invert-isoʳ α⁻¹′ = associator.isoˡ - invert-isoʳ ƛ′ = unitorˡ.isoʳ - invert-isoʳ ƛ⁻¹′ = unitorˡ.isoˡ - invert-isoʳ ρ′ = unitorʳ.isoʳ - invert-isoʳ ρ⁻¹′ = unitorʳ.isoˡ -- Helper lemma for showing that mapping into a normal form then back out -- is identity. @@ -313,8 +368,29 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ≈⟨ preserves-≈ f ⟩⊗⟨ preserves-≈ g ⟩ [ f ↓] ⊗₁ [ g ↓] ∎ - preserves-≈ (α′ {A} {B} {C}) = {!!} - preserves-≈ α⁻¹′ = {!!} + preserves-≈ (α′ {A} {B} {C}) = begin + ([ invert (into A) ↓] ⊗₁ (([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓]) ∘ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓]) ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C)) ↓]) ∘ + [ ⌊ αⁿ (nf₀ A) (nf₀ B) (nf₀ C) ⌋ ↓] ∘ [ ⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C) ↓] ∘ + (([ ⌞⌟-⊗ (nf₀ A) (nf₀ B) ↓] ∘ [ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓]) + ≈⟨ {!!} ⟩ + [ invert (into A) ↓] ⊗₁ ([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓]) ∘ + (id ⊗₁ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓] ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C)) ↓] ∘ [ ⌊ αⁿ (nf₀ A) (nf₀ B) (nf₀ C) ⌋ ↓] ∘ [ ⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C) ↓] ∘ [ ⌞⌟-⊗ (nf₀ A) (nf₀ B) ↓] ⊗₁ id) ∘ + (([ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓]) + ≈⟨ refl⟩∘⟨ ( refl⟩∘⟨ refl⟩∘⟨ (⌊⌋-α (nf₀ A) (nf₀ B) (nf₀ C))) ⟩∘⟨refl ⟩ + [ invert (into A) ↓] ⊗₁ ([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓]) ∘ + (id ⊗₁ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓] ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C)) ↓] ∘ [ ⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C) ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ (nf₀ B) (nf₀ C) ↓] ∘ associator.from) ∘ + (([ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓]) + ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ cancelˡ (invert-isoˡ (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C)))) ⟩∘⟨refl ⟩ + [ invert (into A) ↓] ⊗₁ ([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓]) ∘ + (id ⊗₁ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ (nf₀ B) (nf₀ C) ↓] ∘ associator.from) ∘ + (([ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓]) + ≈⟨ refl⟩∘⟨ cancelˡ (⊗-elim identity² (invert-isoˡ (⌞⌟-⊗ (nf₀ B) (nf₀ C)))) ⟩∘⟨refl ⟩ + [ invert (into A) ↓] ⊗₁ ([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓]) ∘ associator.from ∘ (([ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓]) + ≈⟨ pushʳ assoc-commute-from ⟩ + ([ invert (into A) ↓] ⊗₁ ([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓]) ∘ ([ into A ↓] ⊗₁ ([ into B ↓] ⊗₁ [ into C ↓]))) ∘ associator.from + ≈⟨ elimˡ (⊗-elim (invert-isoˡ (into A)) (⊗-elim (invert-isoˡ (into B)) (invert-isoˡ (into C)))) ⟩ + associator.from ∎ + preserves-≈ (α⁻¹′ {A} {B} {C}) = {!!} preserves-≈ (ƛ′ {A}) = begin [ out A ↓] ∘ id ∘ unitorˡ.from ∘ id ⊗₁ [ into A ↓] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-from ⟩ [ out A ↓] ∘ id ∘ [ into A ↓] ∘ unitorˡ.from ≈˘⟨ assoc²' ⟩ @@ -339,9 +415,5 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where [ out A ↓] ⊗₁ id ∘ unitorʳ.to ∘ [ into A ↓] ≈⟨ refl⟩∘⟨ unitorʳ-commute-to ⟩ [ out A ↓] ⊗₁ id ∘ [ into A ↓] ⊗₁ id ∘ unitorʳ.to - ≈⟨ pullˡ (⟺ ⊗.homomorphism) ⟩ - ([ out A ↓] ∘ [ into A ↓]) ⊗₁ (id ∘ id) ∘ unitorʳ.to - ≈⟨ (invert-isoˡ (into A) ⟩⊗⟨ identity²) ⟩∘⟨refl ⟩ - id ⊗₁ id ∘ unitorʳ.to - ≈⟨ elimˡ ⊗.identity ⟩ + ≈⟨ cancelˡ (⊗-elim (invert-isoˡ (into A)) identity²) ⟩ unitorʳ.to ∎ From dde08b7f931656874af47c2d10fed6ceed8c6ab1 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Sat, 8 May 2021 12:03:27 -0700 Subject: [PATCH 6/7] Finish the proof that normalization respects equality --- src/Categories/Tactic/Monoidal.agda | 64 ++++++++++++++++++++++++----- 1 file changed, 53 insertions(+), 11 deletions(-) diff --git a/src/Categories/Tactic/Monoidal.agda b/src/Categories/Tactic/Monoidal.agda index fe859808d..8c8f13d85 100644 --- a/src/Categories/Tactic/Monoidal.agda +++ b/src/Categories/Tactic/Monoidal.agda @@ -372,7 +372,17 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ([ invert (into A) ↓] ⊗₁ (([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓]) ∘ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓]) ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C)) ↓]) ∘ [ ⌊ αⁿ (nf₀ A) (nf₀ B) (nf₀ C) ⌋ ↓] ∘ [ ⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C) ↓] ∘ (([ ⌞⌟-⊗ (nf₀ A) (nf₀ B) ↓] ∘ [ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓]) - ≈⟨ {!!} ⟩ + ≈⟨ pushˡ split₂ʳ ⟩∘⟨refl ⟩ + ([ invert (into A) ↓] ⊗₁ [ invert (into B) ↓] ⊗₁ [ invert (into C) ↓] ∘ id ⊗₁ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓] ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C)) ↓]) ∘ + [ ⌊ αⁿ (nf₀ A) (nf₀ B) (nf₀ C) ⌋ ↓] ∘ + [ ⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C) ↓] ∘ + ([ ⌞⌟-⊗ (nf₀ A) (nf₀ B) ↓] ∘ [ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓] + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushʳ split₁ˡ ⟩ + ([ invert (into A) ↓] ⊗₁ [ invert (into B) ↓] ⊗₁ [ invert (into C) ↓] ∘ id ⊗₁ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓] ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C)) ↓]) ∘ + [ ⌊ αⁿ (nf₀ A) (nf₀ B) (nf₀ C) ⌋ ↓] ∘ + ([ ⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C) ↓] ∘ [ ⌞⌟-⊗ (nf₀ A) (nf₀ B) ↓] ⊗₁ id) ∘ + ([ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓] + ≈⟨ assoc²' ○ (refl⟩∘⟨ (⟺ assoc²' ○ pullˡ assoc²')) ⟩ [ invert (into A) ↓] ⊗₁ ([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓]) ∘ (id ⊗₁ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓] ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C)) ↓] ∘ [ ⌊ αⁿ (nf₀ A) (nf₀ B) (nf₀ C) ⌋ ↓] ∘ [ ⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C) ↓] ∘ [ ⌞⌟-⊗ (nf₀ A) (nf₀ B) ↓] ⊗₁ id) ∘ (([ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓]) @@ -390,16 +400,49 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ([ invert (into A) ↓] ⊗₁ ([ invert (into B) ↓] ⊗₁ [ invert (into C) ↓]) ∘ ([ into A ↓] ⊗₁ ([ into B ↓] ⊗₁ [ into C ↓]))) ∘ associator.from ≈⟨ elimˡ (⊗-elim (invert-isoˡ (into A)) (⊗-elim (invert-isoˡ (into B)) (invert-isoˡ (into C)))) ⟩ associator.from ∎ - preserves-≈ (α⁻¹′ {A} {B} {C}) = {!!} + preserves-≈ (α⁻¹′ {A} {B} {C}) = begin + ((([ invert (into A) ↓] ⊗₁ [ invert (into B) ↓] ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B)) ↓]) ⊗₁ [ invert (into C) ↓]) ∘ [ invert (⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C)) ↓]) ∘ + [ ⌊ invertⁿ (αⁿ (nf₀ A) (nf₀ B) (nf₀ C)) ⌋ ↓] ∘ + [ ⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C) ↓] ∘ + [ into A ↓] ⊗₁ ([ ⌞⌟-⊗ (nf₀ B) (nf₀ C) ↓] ∘ [ into B ↓] ⊗₁ [ into C ↓]) + ≈⟨ (pushˡ split₁ʳ) ⟩∘⟨ (refl⟩∘⟨ pushʳ split₂ˡ) ⟩ + (([ invert (into A) ↓] ⊗₁ [ invert (into B) ↓]) ⊗₁ [ invert (into C) ↓] ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B)) ↓] ⊗₁ id ∘ [ invert (⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C)) ↓]) ∘ + [ ⌊ invertⁿ (αⁿ (nf₀ A) (nf₀ B) (nf₀ C)) ⌋ ↓] ∘ + ([ ⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C) ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ (nf₀ B) (nf₀ C) ↓]) ∘ + [ into A ↓] ⊗₁ [ into B ↓] ⊗₁ [ into C ↓] + ≈⟨ assoc ○ (refl⟩∘⟨ (⟺ assoc)) ⟩ + ([ invert (into A) ↓] ⊗₁ [ invert (into B) ↓]) ⊗₁ [ invert (into C) ↓] ∘ + (([ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B)) ↓] ⊗₁ id ∘ [ invert (⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C)) ↓]) ∘ [ ⌊ invertⁿ (αⁿ (nf₀ A) (nf₀ B) (nf₀ C)) ⌋ ↓]) ∘ + ([ ⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C) ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ (nf₀ B) (nf₀ C) ↓]) ∘ + [ into A ↓] ⊗₁ ([ into B ↓] ⊗₁ [ into C ↓]) + ≈⟨ (refl⟩∘⟨ ⌊⌋-invert (⌞⌟-⊗ (nf₀ A ++ nf₀ B) (nf₀ C) ∘′ ⌞⌟-⊗ (nf₀ A) (nf₀ B) ⊗₁′ id′) (αⁿ (nf₀ A) (nf₀ B) (nf₀ C)) (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C) ∘′ id′ ⊗₁′ ⌞⌟-⊗ (nf₀ B) (nf₀ C) ∘′ α′) (⌊⌋-α (nf₀ A) (nf₀ B) (nf₀ C)) ⟩∘⟨refl) ⟩ + ([ invert (into A) ↓] ⊗₁ [ invert (into B) ↓]) ⊗₁ [ invert (into C) ↓] ∘ + ((associator.to ∘ (id ⊗₁ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓])) ∘ [ invert (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C)) ↓]) ∘ + ([ ⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C) ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ (nf₀ B) (nf₀ C) ↓]) ∘ [ into A ↓] ⊗₁ ([ into B ↓] ⊗₁ [ into C ↓]) + ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (cancelʳ (invert-isoˡ (⌞⌟-⊗ (nf₀ A) (nf₀ B ++ nf₀ C))))) ⟩ + ([ invert (into A) ↓] ⊗₁ [ invert (into B) ↓]) ⊗₁ [ invert (into C) ↓] ∘ + ((associator.to ∘ id ⊗₁ [ invert (⌞⌟-⊗ (nf₀ B) (nf₀ C)) ↓]) ∘ id ⊗₁ [ ⌞⌟-⊗ (nf₀ B) (nf₀ C) ↓]) ∘ + [ into A ↓] ⊗₁ [ into B ↓] ⊗₁ [ into C ↓] + ≈⟨ refl⟩∘⟨ cancelʳ (⊗-elim identity² (invert-isoˡ (⌞⌟-⊗ (nf₀ B) (nf₀ C)))) ⟩∘⟨refl ⟩ + ([ invert (into A) ↓] ⊗₁ [ invert (into B) ↓]) ⊗₁ [ invert (into C) ↓] ∘ associator.to ∘ [ into A ↓] ⊗₁ [ into B ↓] ⊗₁ [ into C ↓] + ≈⟨ pushʳ assoc-commute-to ⟩ + (([ invert (into A) ↓] ⊗₁ [ invert (into B) ↓]) ⊗₁ [ invert (into C) ↓] ∘ ([ into A ↓] ⊗₁ [ into B ↓]) ⊗₁ [ into C ↓]) ∘ associator.to + ≈⟨ elimˡ (⊗-elim (⊗-elim (invert-isoˡ (into A)) (invert-isoˡ (into B))) (invert-isoˡ (into C))) ⟩ + associator.to ∎ preserves-≈ (ƛ′ {A}) = begin - [ out A ↓] ∘ id ∘ unitorˡ.from ∘ id ⊗₁ [ into A ↓] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-from ⟩ - [ out A ↓] ∘ id ∘ [ into A ↓] ∘ unitorˡ.from ≈˘⟨ assoc²' ⟩ - ([ out A ↓] ∘ id ∘ [ into A ↓]) ∘ unitorˡ.from ≈⟨ elimˡ (into-out A) ⟩ - unitorˡ.from ∎ + [ out A ↓] ∘ id ∘ unitorˡ.from ∘ id ⊗₁ [ into A ↓] + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-from ⟩ + [ out A ↓] ∘ id ∘ [ into A ↓] ∘ unitorˡ.from + ≈˘⟨ assoc²' ⟩ + ([ out A ↓] ∘ id ∘ [ into A ↓]) ∘ unitorˡ.from + ≈⟨ elimˡ (into-out A) ⟩ + unitorˡ.from ∎ preserves-≈ (ƛ⁻¹′ {A}) = begin - (id ⊗₁ [ out A ↓] ∘ unitorˡ.to) ∘ id ∘ [ into A ↓] ≈˘⟨ unitorˡ-commute-to ⟩∘⟨refl ⟩ - (unitorˡ.to ∘ [ out A ↓]) ∘ id ∘ [ into A ↓] ≈⟨ cancelʳ (into-out A) ⟩ - unitorˡ.to ∎ + (id ⊗₁ [ out A ↓] ∘ unitorˡ.to) ∘ id ∘ [ into A ↓] + ≈˘⟨ unitorˡ-commute-to ⟩∘⟨refl ⟩ + (unitorˡ.to ∘ [ out A ↓]) ∘ id ∘ [ into A ↓] + ≈⟨ cancelʳ (into-out A) ⟩ + unitorˡ.to ∎ preserves-≈ (ρ′ {A}) = begin [ out A ↓] ∘ [ ⌊ ρⁿ (nf₀ A) ⌋ ↓] ∘ [ ⌞⌟-⊗ (nf₀ A) [] ↓] ∘ [ into A ↓] ⊗₁ id ≈⟨ refl⟩∘⟨ pullˡ (⌊⌋-ρ (nf₀ A)) ⟩ @@ -407,8 +450,7 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ≈⟨ refl⟩∘⟨ unitorʳ-commute-from ⟩ [ out A ↓] ∘ [ into A ↓] ∘ unitorʳ.from ≈⟨ cancelˡ (invert-isoˡ (into A)) ⟩ - unitorʳ.from - ∎ + unitorʳ.from ∎ preserves-≈ (ρ⁻¹′ {A}) = begin ([ out A ↓] ⊗₁ id ∘ [ invert (⌞⌟-⊗ (nf₀ A) []) ↓]) ∘ ([ ⌊ invertⁿ (ρⁿ (nf₀ A)) ⌋ ↓] ∘ [ into A ↓]) ≈⟨ center (⌊⌋-invert (⌞⌟-⊗ (nf₀ A) []) (ρⁿ (nf₀ A)) ρ′ (⌊⌋-ρ (nf₀ A))) ⟩ From a10b7d219867a26880f6743dca469797d074f206 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Sat, 8 May 2021 12:08:30 -0700 Subject: [PATCH 7/7] Clean up some proofs --- src/Categories/Tactic/Monoidal.agda | 41 +++++++++-------------------- 1 file changed, 12 insertions(+), 29 deletions(-) diff --git a/src/Categories/Tactic/Monoidal.agda b/src/Categories/Tactic/Monoidal.agda index 8c8f13d85..8e5ffab46 100644 --- a/src/Categories/Tactic/Monoidal.agda +++ b/src/Categories/Tactic/Monoidal.agda @@ -218,6 +218,14 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ⌞⌟-⊗ [] M = ƛ′ ⌞⌟-⊗ (X ∷ N) M = id′ ⊗₁′ ⌞⌟-⊗ N M ∘′ α′ + subst-∷-⊗ : ∀ {X N M} (eq : N ≡ M) → + subst (NfExpr (X ∷ N)) (cong (X ∷_) eq) (idⁿ ⊗ⁿ idⁿ {N}) ≡ + idⁿ ⊗ⁿ subst (NfExpr N) eq idⁿ + subst-∷-⊗ refl = refl + + ⌊⌋-identityˡ : ∀ {X N M} (f : NfExpr N M) → ⌊ idⁿ ⊗ⁿ f ⌋ ≈↓ id′ {X ′} ⊗₁′ ⌊ f ⌋ + ⌊⌋-identityˡ idⁿ = ⟺ ⊗.identity + ⌊⌋-⊗ : ∀ {N₁ N₂ M₁ M₂} (f : NfExpr N₁ M₁) (g : NfExpr N₂ M₂) → ⌊ f ⊗ⁿ g ⌋ ∘′ ⌞⌟-⊗ N₁ N₂ ≈↓ ⌞⌟-⊗ M₁ M₂ ∘′ ⌊ f ⌋ ⊗₁′ ⌊ g ⌋ ⌊⌋-⊗ {N₁} {N₂} idⁿ idⁿ = begin @@ -230,28 +238,15 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ⌊⌋-ρ (X ∷ N) = begin [ ⌊ subst (NfExpr (X ∷ N ++ [])) (cong (X ∷_) (++-identityʳ N)) idⁿ ⌋ ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from - ≡⟨ cong (λ f → [ ⌊ f ⌋ ∘′ id′ ⊗₁′ ⌞⌟-⊗ N [] ∘′ α′ ↓]) - (helper₁ (++-identityʳ N)) ⟩ + ≡⟨ cong (λ f → [ ⌊ f ⌋ ∘′ id′ ⊗₁′ ⌞⌟-⊗ N [] ∘′ α′ ↓]) (subst-∷-⊗ (++-identityʳ N)) ⟩ [ ⌊ idⁿ ⊗ⁿ ρⁿ N ⌋ ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from - ≈⟨ helper₂ (ρⁿ N) ⟩∘⟨refl ⟩ + ≈⟨ ⌊⌋-identityˡ (ρⁿ N) ⟩∘⟨refl ⟩ id ⊗₁ [ ⌊ ρⁿ N ⌋ ↓] ∘ id ⊗₁ [ ⌞⌟-⊗ N [] ↓] ∘ associator.from ≈⟨ merge₂ ⌊⌋-ρ N ⟩∘⟨ Equiv.refl ⟩ id ⊗₁ unitorʳ.from ∘ associator.from ≈⟨ Kelly's.coherence₂ 𝒱 ⟩ unitorʳ.from ∎ - where - - -- FIXME: give these better names and reuse them in the proof of - -- the hexagon identity (the ⌊⌋-α yet to be written). - - helper₁ : ∀ {X N M} (eq : N ≡ M) → - subst (NfExpr (X ∷ N)) (cong (X ∷_) eq) (idⁿ ⊗ⁿ idⁿ {N}) ≡ - idⁿ ⊗ⁿ subst (NfExpr N) eq idⁿ - helper₁ refl = refl - - helper₂ : ∀ {X N M} (f : NfExpr N M) → ⌊ idⁿ ⊗ⁿ f ⌋ ≈↓ id′ {X ′} ⊗₁′ ⌊ f ⌋ - helper₂ idⁿ = ⟺ ⊗.identity ⌊⌋-α : ∀ N₁ N₂ N₃ → ⌊ αⁿ N₁ N₂ N₃ ⌋ ∘′ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ∘′ ⌞⌟-⊗ N₁ N₂ ⊗₁′ id′ ≈↓ ⌞⌟-⊗ N₁ (N₂ ++ N₃) ∘′ id′ ⊗₁′ (⌞⌟-⊗ N₂ N₃) ∘′ α′ ⌊⌋-α [] N₂ N₃ = begin @@ -262,11 +257,11 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ⌊⌋-α (X ∷ N₁) N₂ N₃ = begin [ ⌊ subst (NfExpr (X ∷ (N₁ ++ N₂) ++ N₃)) (cong (_∷_ X) (++-assoc N₁ N₂ N₃)) idⁿ ⌋ ↓] ∘ (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ (id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ associator.from) ⊗₁ id - ≡⟨ cong (λ f → [ ⌊ f ⌋ ↓] ∘ (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ (id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ associator.from) ⊗₁ id) (helper₁ (++-assoc N₁ N₂ N₃)) ⟩ + ≡⟨ cong (λ f → [ ⌊ f ⌋ ↓] ∘ (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ (id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ associator.from) ⊗₁ id) (subst-∷-⊗ (++-assoc N₁ N₂ N₃)) ⟩ [ ⌊ idⁿ ⊗ⁿ subst (NfExpr ((N₁ ++ N₂) ++ N₃)) (++-assoc N₁ N₂ N₃) idⁿ ⌋ ↓] ∘ (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ (id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓] ∘ associator.from) ⊗₁ id - ≈⟨ helper₂ (subst (NfExpr ((N₁ ++ N₂) ++ N₃)) (++-assoc N₁ N₂ N₃) idⁿ) ⟩∘⟨refl ⟩ + ≈⟨ ⌊⌋-identityˡ (subst (NfExpr ((N₁ ++ N₂) ++ N₃)) (++-assoc N₁ N₂ N₃) idⁿ) ⟩∘⟨refl ⟩ (id ⊗₁ [ ⌊ αⁿ N₁ N₂ N₃ ⌋ ↓]) ∘ (id ⊗₁ [ ⌞⌟-⊗ (N₁ ++ N₂) N₃ ↓] ∘ associator.from) ∘ ((id ⊗₁ [ ⌞⌟-⊗ N₁ N₂ ↓]) ∘ associator.from) ⊗₁ id @@ -292,18 +287,6 @@ module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝒱 : Monoidal 𝒞) where ≈⟨ (refl⟩∘⟨ (⊗.identity ⟩⊗⟨refl) ⟩∘⟨refl) ⟩ (id ⊗₁ [ ⌞⌟-⊗ N₁ (N₂ ++ N₃) ↓] ∘ associator.from) ∘ (id ⊗₁ [ ⌞⌟-⊗ N₂ N₃ ↓] ∘ associator.from) ∎ - where - - -- FIXME: give these better names and reuse them in the proof of - -- the hexagon identity (the ⌊⌋-α yet to be written). - - helper₁ : ∀ {X N M} (eq : N ≡ M) → - subst (NfExpr (X ∷ N)) (cong (X ∷_) eq) (idⁿ ⊗ⁿ idⁿ {N}) ≡ - idⁿ ⊗ⁿ subst (NfExpr N) eq idⁿ - helper₁ refl = refl - - helper₂ : ∀ {X N M} (f : NfExpr N M) → ⌊ idⁿ ⊗ⁿ f ⌋ ≈↓ id′ {X ′} ⊗₁′ ⌊ f ⌋ - helper₂ idⁿ = ⟺ ⊗.identity ⌊⌋-invert : ∀ {M} {N O} (f : Expr M ⌞ N ⌟) (g : NfExpr N O) (h : Expr M ⌞ O ⌟) → ⌊ g ⌋ ∘′ f ≈↓ h → invert f ∘′ ⌊ invertⁿ g ⌋ ≈↓ invert h ⌊⌋-invert f idⁿ h eq = begin