diff --git a/Cubical.Categories.Category.Precategory.html b/Cubical.Categories.Category.Precategory.html deleted file mode 100644 index 795882f3a2..0000000000 --- a/Cubical.Categories.Category.Precategory.html +++ /dev/null @@ -1,340 +0,0 @@ - -Cubical.Categories.Category.Precategory
{-# OPTIONS --safe #-}
-module Cubical.Categories.Category.Precategory where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Data.Sigma renaming (_×_ to _×'_)
-
-open import Cubical.Foundations.Pointed hiding (⋆ ; id)
-
-private
-  variable
-    ℓ ℓ' : Level
-
--- Precategories
-record Precategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
-  -- no-eta-equality ; NOTE: need eta equality for `opop`
-  field
-    ob : Type ℓ
-    Hom[_,_] : ob → ob → Type ℓ'
-    id   : ∀ {x} → Hom[ x , x ]
-    _⋆_  : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
-    ⋆IdL : ∀ {x y} (f : Hom[ x , y ]) → id ⋆ f ≡ f
-    ⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ id ≡ f
-    ⋆Assoc : ∀ {u v w x} (f : Hom[ u , v ]) (g : Hom[ v , w ]) (h : Hom[ w , x ])
-      → (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h)
-
-  -- composition: alternative to diagramatic order
-  _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ]
-  g ∘ f = f ⋆ g
-
-open Precategory
-
--- Helpful syntax/notation
-_[_,_] : (C : Precategory ℓ ℓ') → (x y : C .ob) → Type ℓ'
-_[_,_] = Hom[_,_]
-
--- Needed to define this in order to be able to make the subsequence syntax declaration
-seq' : ∀ (C : Precategory ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
-seq' = _⋆_
-
-infixl 15 seq'
-syntax seq' C f g = f ⋆⟨ C ⟩ g
-
--- composition
-comp' : ∀ (C : Precategory ℓ ℓ') {x y z} (g : C [ y , z ]) (f : C [ x , y ]) → C [ x , z ]
-comp' = _∘_
-
-infixr 16 comp'
-syntax comp' C g f = g ∘⟨ C ⟩ f
-
--- Isomorphisms and paths in precategories
-record PrecatIso (C : Precategory ℓ ℓ') (x y : C .ob) : Type ℓ' where
-  constructor precatiso
-  field
-    mor : C [ x , y ]
-    inv : C [ y , x ]
-    sec : inv ⋆⟨ C ⟩ mor ≡ C .id
-    ret : mor ⋆⟨ C ⟩ inv ≡ C .id
-
--- Opposite precategory
-_^op : Precategory ℓ ℓ' → Precategory ℓ ℓ'
-(C ^op) .ob = C .ob
-(C ^op) .Hom[_,_] x y = C .Hom[_,_] y x
-(C ^op) .id = C .id
-(C ^op) ._⋆_ f g = C ._⋆_ g f
-(C ^op) .⋆IdL = C .⋆IdR
-(C ^op) .⋆IdR = C .⋆IdL
-(C ^op) .⋆Assoc f g h = sym (C .⋆Assoc _ _ _)
-
--- Natural isomorphisms
-module _ {ℓC ℓC' : Level} {C : Precategory ℓC ℓC'}
-  {x y : C .ob} (f : Hom[_,_] C x y) where
-  record preIsIso : Type (ℓ-max ℓC ℓC') where
-    field
-      inv' : Hom[_,_] C y x
-      sect : _⋆_ C inv' f ≡ id C {y}
-      retr : _⋆_ C f inv' ≡ id C {x}
-
-open Precategory
-open preIsIso
-
-module _ {ℓC ℓC' ℓD ℓD' : Level} where
- -- Products
- _×_ :  (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') → Precategory _ _
- ob (C × D) = ob C ×' ob D
- Hom[_,_] (C × D) (c , d) (c' , d') =
-   Hom[_,_] C c c' ×' Hom[_,_] D d d'
- id (C × D) = id C , id D
- _⋆_ (C × D) f g = _⋆_ C (fst f) (fst g) , _⋆_ D (snd f) (snd g)
- ⋆IdL (C × D) (f , g) i = (⋆IdL C f i) , (⋆IdL D g i)
- ⋆IdR (C × D) (f , g) i = (⋆IdR C f i) , (⋆IdR D g i)
- ⋆Assoc (C × D) (f , g) (f' , g') (f'' , g'') i =
-   ⋆Assoc C f f' f'' i , ⋆Assoc D g g' g'' i
-
- -- Functors
- record Prefunctor (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') :
-          Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
-   no-eta-equality
-
-   field
-     F-ob  : C .ob → D .ob
-     F-hom : {x y : C .ob} → C [ x , y ] → D [ F-ob x , F-ob y ]
-     F-id  : {x : C .ob} → F-hom {y = x} (id C) ≡ id D
-     F-seq : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ])
-           → F-hom (f ⋆⟨ C ⟩ g) ≡ (F-hom f) ⋆⟨ D ⟩ (F-hom g)
-
- -- Natural transformation
- record PreNatTrans (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD')
-          (F G : Prefunctor C D) :
-          Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
-   no-eta-equality
-
-   open Prefunctor
-
-   field
-     N-ob : (x : C .ob) → D [ F .F-ob x , G .F-ob x ]
-     N-hom : {x y : C .ob} (f : C [ x , y ])
-       → (F .F-hom f) ⋆⟨ D ⟩ (N-ob y) ≡ (N-ob x) ⋆⟨ D ⟩ (G .F-hom f)
-
- -- Natural isomorphisms
- record PreNatIso (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD')
-          (F G : Prefunctor C D) :
-          Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
-   open PreNatTrans
-
-   field
-     trans : PreNatTrans C D F G
-     isIs : (c : C .ob) → preIsIso {C = D} (trans .N-ob c)
-
-open Prefunctor
-open PreNatTrans
-open PreNatIso
-open preIsIso
-
-
-module _ {ℓC ℓC' ℓD ℓD' : Level}
-  {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'}
-  (F G H : Prefunctor C D) where
-
-  compPreNatTrans : PreNatTrans _ _ F G → PreNatTrans _ _ G H → PreNatTrans _ _ F H
-  N-ob (compPreNatTrans η γ) c = N-ob η c ⋆⟨ D ⟩ N-ob γ c
-  N-hom (compPreNatTrans η γ) {x = x} {y = y} f =
-    sym (⋆Assoc D _ _ _) ∙ cong (λ w → w ⋆⟨ D ⟩ (N-ob γ y)) (N-hom η f)
-    ∙ ⋆Assoc D _ _ _
-    ∙ cong  (D ⋆ N-ob η x) (N-hom γ f)
-    ∙ sym (⋆Assoc D _ _ _)
-
-  compPreNatIso : PreNatIso _ _ F G → PreNatIso _ _ G H → PreNatIso _ _ F H
-  trans (compPreNatIso isη isγ) = compPreNatTrans (trans isη) (trans isγ)
-  inv' (isIs (compPreNatIso isη isγ) c) = inv' (isIs isγ c) ⋆⟨ D ⟩ (inv' (isIs isη c))
-  sect (isIs (compPreNatIso isη isγ) c) =
-    ⋆Assoc D _ _ _
-    ∙ cong (D ⋆ inv' (isIs isγ c))
-       (sym (⋆Assoc D _ _ _)
-       ∙ cong (λ w → w ⋆⟨ D ⟩ (N-ob (trans isγ) c)) (sect (isIs isη c))
-       ∙ ⋆IdL D _)
-    ∙ sect (isIs isγ c)
-  retr (isIs (compPreNatIso isη isγ) c) =
-    ⋆Assoc D _ _ _
-    ∙ cong (D ⋆ N-ob (trans isη) c)
-        (sym (⋆Assoc D _ _ _)
-        ∙ cong (λ w → w ⋆⟨ D ⟩ (inv' (isIs isη c))) (retr (isIs isγ c))
-        ∙ ⋆IdL D _)
-    ∙ retr (isIs isη c)
-
-module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level}
-  {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} {E : Precategory ℓE ℓE'}
- where
- comp-Prefunctor : (F : Prefunctor C D) (G : Prefunctor D E)
-   → Prefunctor C E
- F-ob (comp-Prefunctor F G) c = F-ob G (F-ob F c)
- F-hom (comp-Prefunctor F G) f = F-hom G (F-hom F f)
- F-id (comp-Prefunctor F G) = cong (F-hom G) (F-id F) ∙ F-id G
- F-seq (comp-Prefunctor F G) f g = cong (F-hom G) (F-seq F f g) ∙ F-seq G _ _
-
-
-module _ {ℓC ℓC' : Level} {C : Precategory ℓC ℓC'}
-  (F : Prefunctor (C × C) C) where
-  assocₗ : Prefunctor (C × (C × C)) C
-  F-ob assocₗ (x , y , z) = F-ob F (x , F-ob F (y , z))
-  F-hom assocₗ {x} {y} (f , g) = F-hom F (f , F-hom F g)
-  F-id assocₗ =
-    cong (λ y → F-hom F (id C , y)) (F-id {C = C × C} F)
-      ∙ F-id F
-  F-seq assocₗ f g =
-    cong (F-hom F)
-         (cong (fst (f ⋆⟨ C × (C × C) ⟩ g) ,_)
-           (F-seq F (snd f) (snd g)))
-       ∙ F-seq F _ _
-
-  assocᵣ : Prefunctor (C × (C × C)) C
-  F-ob assocᵣ (x , y , z) = F-ob F (F-ob F (x , y) , z)
-  F-hom assocᵣ (f , g) = F-hom F (F-hom F (f , (fst g)) , snd g)
-  F-id assocᵣ = cong (F-hom F) (cong (_, id C) (F-id F))
-              ∙ F-id F
-  F-seq assocᵣ (f , f' , f'') (g , g' , g'') =
-    cong (F-hom F) (cong (_, _⋆_ C f'' g'')
-      (F-seq F (f , f') (g , g')))
-    ∙ F-seq F _ _
-
--- Left and right restrictions of functors
-module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level}
-      {C : Precategory ℓC ℓC'}
-      {D : Precategory ℓD ℓD'}
-      {E : Precategory ℓE ℓE'}
-      where
- restrFunctorₗ : (F : Prefunctor (C × D) E) (c : C . ob)
-   → Prefunctor D E
- F-ob (restrFunctorₗ F c) d = F-ob F (c , d)
- F-hom (restrFunctorₗ F c) f = F-hom F (id C , f)
- F-id (restrFunctorₗ F c) = F-id F
- F-seq (restrFunctorₗ F c) f g =
-     cong (F-hom F) (ΣPathP (sym (⋆IdR C _) , refl))
-   ∙ F-seq F (id C , f) (id C , g)
-
- restrFunctorᵣ : (F : Prefunctor (C × D) E) (d : D . ob)
-   → Prefunctor C E
- F-ob (restrFunctorᵣ F d) c = F-ob F (c , d)
- F-hom (restrFunctorᵣ F d) f = F-hom F (f , (id D))
- F-id (restrFunctorᵣ F d) = F-id F
- F-seq (restrFunctorᵣ F d) f g =
-     cong (F-hom F) (ΣPathP (refl , sym (⋆IdR D _)))
-   ∙ F-seq F (f , id D) (g , id D)
-
--- Identity functor
-idPrefunctor : {ℓC ℓC' : Level}
-      (C : Precategory ℓC ℓC')
-   → Prefunctor C C
-Prefunctor.F-ob (idPrefunctor C) c = c
-Prefunctor.F-hom (idPrefunctor C) x = x
-Prefunctor.F-id (idPrefunctor C) = refl
-Prefunctor.F-seq (idPrefunctor C) _ _ = refl
-
--- Commutator
-commFunctor : {ℓC ℓC' ℓD ℓD' : Level}
-      {C : Precategory ℓC ℓC'}
-      {D : Precategory ℓD ℓD'}
-   → Prefunctor (C × D) (D × C)
-Prefunctor.F-ob commFunctor (x , y) = y , x
-Prefunctor.F-hom commFunctor (f , g) = g , f
-Prefunctor.F-id commFunctor = refl
-Prefunctor.F-seq commFunctor _ _ = refl
-
--- Monoidal, braided and monoidal symmetric precategories
-module _ (M : Precategory ℓ ℓ') where
-  record isMonoidalPrecategory : Type (ℓ-max ℓ ℓ') where
-    field
-      _⊗_ : Prefunctor (M × M) M
-      𝟙 : ob M
-
-      ⊗assoc : PreNatIso (M × (M × M)) M (assocₗ _⊗_) (assocᵣ _⊗_)
-
-      ⊗lUnit : PreNatIso M M (restrFunctorₗ _⊗_ 𝟙) (idPrefunctor M)
-      ⊗rUnit : PreNatIso M M (restrFunctorᵣ _⊗_ 𝟙) (idPrefunctor M)
-
-    private
-      α = N-ob (trans ⊗assoc)
-      α⁻ : (c : ob M ×' ob M ×' ob M) → M [ _ , _ ]
-      α⁻ c = preIsIso.inv' (isIs ⊗assoc c)
-      rId = N-ob (trans ⊗rUnit)
-      lId = N-ob (trans ⊗lUnit)
-
-    field
-      -- Note: associators are on the form x ⊗ (y ⊗ z) → (x ⊗ y) ⊗ z
-      triang : (a b : M .ob)
-        → α (a , 𝟙 , b) ⋆⟨ M ⟩ (F-hom _⊗_ ((rId a) , id M))
-          ≡ F-hom _⊗_ ((id M) , lId b)
-
-      ⊗pentagon : (a b c d : M .ob)
-        → (F-hom _⊗_ (id M , α (b , c , d)))
-           ⋆⟨ M ⟩ ((α (a , (_⊗_ .F-ob (b , c)) , d))
-           ⋆⟨ M ⟩ (F-hom _⊗_ (α (a , b , c) , id M)))
-        ≡  (α (a , b , (F-ob _⊗_ (c , d))))
-           ⋆⟨ M ⟩ (α((F-ob _⊗_ (a , b)) , c , d))
-
-  module _ (mon : isMonoidalPrecategory) where
-    open isMonoidalPrecategory mon
-    private
-      α = N-ob (trans ⊗assoc)
-      α⁻ : (c : ob M ×' ob M ×' ob M) → M [ _ , _ ]
-      α⁻ c = preIsIso.inv' (isIs ⊗assoc c)
-
-    BraidingIsoType : Type _
-    BraidingIsoType = PreNatIso (M × M) M _⊗_ (comp-Prefunctor commFunctor _⊗_)
-
-    HexagonType₁ : (B : BraidingIsoType) → Type _
-    HexagonType₁ B = (x y z : M .ob) →
-      F-hom _⊗_ ((id M) , N-ob (trans B) (y , z))
-        ⋆⟨ M ⟩ α (x , z , y)
-        ⋆⟨ M ⟩ F-hom _⊗_ (N-ob (trans B) (x , z) , (id M))
-       ≡ α (x , y , z)
-        ⋆⟨ M ⟩ N-ob (trans B) ((F-ob _⊗_ (x , y)) , z)
-        ⋆⟨ M ⟩ α (z , x , y)
-
-    HexagonType₂ : (B : BraidingIsoType) → Type _
-    HexagonType₂ B = (x y z : M .ob) →
-      F-hom _⊗_ (N-ob (trans B) (x , y) , id M)
-        ⋆⟨ M ⟩ α⁻ (y , x , z)
-        ⋆⟨ M ⟩ F-hom _⊗_ ((id M) , N-ob (trans B) (x , z))
-       ≡ α⁻ (x , y , z)
-        ⋆⟨ M ⟩ N-ob (trans B) (x , F-ob _⊗_ (y , z))
-        ⋆⟨ M ⟩ α⁻ (y , z , x)
-
-    isSymmetricBraiding : (B : BraidingIsoType)
-      → Type _
-    isSymmetricBraiding B = (x y : M .ob) →
-      N-ob (trans B) (x , y) ⋆⟨ M ⟩ (N-ob (trans B) (y , x))
-      ≡ id M
-
-  record isBraidedPrecategory : Type (ℓ-max ℓ ℓ') where
-    open isMonoidalPrecategory
-    field
-      isMonoidal : isMonoidalPrecategory
-      Braid : BraidingIsoType isMonoidal
-      hexagons : (x y z : M .ob)
-        → HexagonType₁ isMonoidal Braid
-        ×' HexagonType₂ isMonoidal Braid
-
-  record isSymmetricPrecategory : Type (ℓ-max ℓ ℓ') where
-    field
-      isMonoidal : isMonoidalPrecategory
-      Braid : BraidingIsoType isMonoidal
-      hexagon : HexagonType₁ isMonoidal Braid
-      symBraiding : isSymmetricBraiding isMonoidal Braid
-
-SymmetricMonoidalPrecat : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
-SymmetricMonoidalPrecat ℓ ℓ' =
-  Σ[ C ∈ Precategory ℓ ℓ' ] isSymmetricPrecategory C
-
--- Instances
-module _ (ℓ : Level) where
-  PointedCat : Precategory (ℓ-suc ℓ) ℓ
-  ob PointedCat = Pointed ℓ
-  Hom[_,_] PointedCat A B = A →∙ B
-  Precategory.id PointedCat = idfun∙ _
-  _⋆_ PointedCat f g = g ∘∙ f
-  ⋆IdL PointedCat = ∘∙-idˡ
-  ⋆IdR PointedCat = ∘∙-idʳ
-  ⋆Assoc PointedCat f g h = sym (∘∙-assoc h g f)
-
\ No newline at end of file diff --git a/Cubical.Categories.Everything.html b/Cubical.Categories.Everything.html index 579dd6e5ac..5aede7cfcf 100644 --- a/Cubical.Categories.Everything.html +++ b/Cubical.Categories.Everything.html @@ -9,87 +9,84 @@ import Cubical.Categories.Adjoint import Cubical.Categories.Category import Cubical.Categories.Category.Path -import Cubical.Categories.Category.Precategory -import Cubical.Categories.Commutativity -import Cubical.Categories.Constructions.BinProduct -import Cubical.Categories.Constructions.Elements -import Cubical.Categories.Constructions.EssentialImage -import Cubical.Categories.Constructions.Free -import Cubical.Categories.Constructions.Free.Category -import Cubical.Categories.Constructions.Free.Functor -import Cubical.Categories.Constructions.FullSubcategory -import Cubical.Categories.Constructions.Lift -import Cubical.Categories.Constructions.Power -import Cubical.Categories.Constructions.Product -import Cubical.Categories.Constructions.Quotient -import Cubical.Categories.Constructions.Slice -import Cubical.Categories.Constructions.SubObject -import Cubical.Categories.Constructions.TwistedArrow -import Cubical.Categories.Displayed.Adjoint -import Cubical.Categories.Displayed.Base -import Cubical.Categories.Displayed.BinProduct -import Cubical.Categories.Displayed.Cartesian -import Cubical.Categories.Displayed.Functor -import Cubical.Categories.Displayed.Instances.Codomain -import Cubical.Categories.Displayed.NaturalTransformation -import Cubical.Categories.Displayed.Properties -import Cubical.Categories.Displayed.Reasoning -import Cubical.Categories.DistLatticeSheaf.Base -import Cubical.Categories.DistLatticeSheaf.ComparisonLemma -import Cubical.Categories.DistLatticeSheaf.Diagram -import Cubical.Categories.DistLatticeSheaf.Extension -import Cubical.Categories.Equivalence -import Cubical.Categories.Equivalence.AdjointEquivalence -import Cubical.Categories.Equivalence.WeakEquivalence -import Cubical.Categories.Functor -import Cubical.Categories.Functor.ComposeProperty -import Cubical.Categories.Functors.Constant -import Cubical.Categories.Functors.HomFunctor -import Cubical.Categories.Instances.AbGroups -import Cubical.Categories.Instances.Categories -import Cubical.Categories.Instances.CommAlgebras -import Cubical.Categories.Instances.CommRings -import Cubical.Categories.Instances.Cospan -import Cubical.Categories.Instances.Discrete -import Cubical.Categories.Instances.DistLattice -import Cubical.Categories.Instances.DistLattices -import Cubical.Categories.Instances.EilenbergMoore -import Cubical.Categories.Instances.FunctorAlgebras -import Cubical.Categories.Instances.Functors -import Cubical.Categories.Instances.Functors.Currying -import Cubical.Categories.Instances.Functors.Endo -import Cubical.Categories.Instances.Groups -import Cubical.Categories.Instances.Lattice -import Cubical.Categories.Instances.Lattices -import Cubical.Categories.Instances.Poset -import Cubical.Categories.Instances.RingAlgebras -import Cubical.Categories.Instances.Rings -import Cubical.Categories.Instances.Semilattice -import Cubical.Categories.Instances.Sets -import Cubical.Categories.Instances.Terminal -import Cubical.Categories.Instances.TypePrecategory -import Cubical.Categories.Instances.ZFunctors -import Cubical.Categories.Isomorphism -import Cubical.Categories.Limits -import Cubical.Categories.Limits.RightKan -import Cubical.Categories.Monad.Base -import Cubical.Categories.Monoidal -import Cubical.Categories.Monoidal.Strict.Monoid -import Cubical.Categories.Morphism -import Cubical.Categories.NaturalTransformation -import Cubical.Categories.Presheaf -import Cubical.Categories.Presheaf.NonPresheaf.Cofree -import Cubical.Categories.Presheaf.NonPresheaf.Forget -import Cubical.Categories.Presheaf.NonPresheaf.Free -import Cubical.Categories.Profunctor -import Cubical.Categories.RezkCompletion -import Cubical.Categories.Site.Cover -import Cubical.Categories.Site.Coverage -import Cubical.Categories.Site.Instances.ZariskiCommRing -import Cubical.Categories.Site.Sheaf -import Cubical.Categories.Site.Sheafification -import Cubical.Categories.Site.Sieve -import Cubical.Categories.TypesOfCategories.TypeCategory -import Cubical.Categories.UnderlyingGraph -import Cubical.Categories.Yoneda +import Cubical.Categories.Commutativity +import Cubical.Categories.Constructions.BinProduct +import Cubical.Categories.Constructions.Elements +import Cubical.Categories.Constructions.EssentialImage +import Cubical.Categories.Constructions.Free +import Cubical.Categories.Constructions.Free.Category +import Cubical.Categories.Constructions.Free.Functor +import Cubical.Categories.Constructions.FullSubcategory +import Cubical.Categories.Constructions.Lift +import Cubical.Categories.Constructions.Power +import Cubical.Categories.Constructions.Product +import Cubical.Categories.Constructions.Quotient +import Cubical.Categories.Constructions.Slice +import Cubical.Categories.Constructions.SubObject +import Cubical.Categories.Constructions.TwistedArrow +import Cubical.Categories.Displayed.Adjoint +import Cubical.Categories.Displayed.Base +import Cubical.Categories.Displayed.BinProduct +import Cubical.Categories.Displayed.Cartesian +import Cubical.Categories.Displayed.Functor +import Cubical.Categories.Displayed.Instances.Codomain +import Cubical.Categories.Displayed.NaturalTransformation +import Cubical.Categories.Displayed.Properties +import Cubical.Categories.Displayed.Reasoning +import Cubical.Categories.DistLatticeSheaf.Base +import Cubical.Categories.DistLatticeSheaf.ComparisonLemma +import Cubical.Categories.DistLatticeSheaf.Diagram +import Cubical.Categories.DistLatticeSheaf.Extension +import Cubical.Categories.Equivalence +import Cubical.Categories.Equivalence.AdjointEquivalence +import Cubical.Categories.Equivalence.WeakEquivalence +import Cubical.Categories.Functor +import Cubical.Categories.Functor.ComposeProperty +import Cubical.Categories.Functors.Constant +import Cubical.Categories.Functors.HomFunctor +import Cubical.Categories.Instances.AbGroups +import Cubical.Categories.Instances.CommAlgebras +import Cubical.Categories.Instances.CommRings +import Cubical.Categories.Instances.Cospan +import Cubical.Categories.Instances.Discrete +import Cubical.Categories.Instances.DistLattice +import Cubical.Categories.Instances.DistLattices +import Cubical.Categories.Instances.EilenbergMoore +import Cubical.Categories.Instances.FunctorAlgebras +import Cubical.Categories.Instances.Functors +import Cubical.Categories.Instances.Functors.Currying +import Cubical.Categories.Instances.Functors.Endo +import Cubical.Categories.Instances.Groups +import Cubical.Categories.Instances.Lattice +import Cubical.Categories.Instances.Lattices +import Cubical.Categories.Instances.Poset +import Cubical.Categories.Instances.RingAlgebras +import Cubical.Categories.Instances.Rings +import Cubical.Categories.Instances.Semilattice +import Cubical.Categories.Instances.Sets +import Cubical.Categories.Instances.Terminal +import Cubical.Categories.Instances.ZFunctors +import Cubical.Categories.Isomorphism +import Cubical.Categories.Limits +import Cubical.Categories.Limits.RightKan +import Cubical.Categories.Monad.Base +import Cubical.Categories.Monoidal +import Cubical.Categories.Monoidal.Strict.Monoid +import Cubical.Categories.Morphism +import Cubical.Categories.NaturalTransformation +import Cubical.Categories.Presheaf +import Cubical.Categories.Presheaf.NonPresheaf.Cofree +import Cubical.Categories.Presheaf.NonPresheaf.Forget +import Cubical.Categories.Presheaf.NonPresheaf.Free +import Cubical.Categories.Profunctor +import Cubical.Categories.RezkCompletion +import Cubical.Categories.Site.Cover +import Cubical.Categories.Site.Coverage +import Cubical.Categories.Site.Instances.ZariskiCommRing +import Cubical.Categories.Site.Sheaf +import Cubical.Categories.Site.Sheafification +import Cubical.Categories.Site.Sieve +import Cubical.Categories.TypesOfCategories.TypeCategory +import Cubical.Categories.UnderlyingGraph +import Cubical.Categories.Yoneda \ No newline at end of file diff --git a/Cubical.Categories.Instances.Categories.html b/Cubical.Categories.Instances.Categories.html deleted file mode 100644 index 163d6a10ec..0000000000 --- a/Cubical.Categories.Instances.Categories.html +++ /dev/null @@ -1,27 +0,0 @@ - -Cubical.Categories.Instances.Categories
-- The (pre)category of (small) categories
-{-# OPTIONS --safe #-}
-
-module Cubical.Categories.Instances.Categories where
-
-open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Category.Precategory
-open import Cubical.Categories.Functor.Base
-open import Cubical.Categories.Functor.Properties
-open import Cubical.Foundations.Prelude
-
-
-module _ (ℓ ℓ' : Level) where
-  open Precategory
-
-  CatPrecategory : Precategory (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-max ℓ ℓ')
-  CatPrecategory .ob = Category ℓ ℓ'
-  CatPrecategory .Hom[_,_] = Functor
-  CatPrecategory .id = 𝟙⟨ _ ⟩
-  CatPrecategory ._⋆_ G H = H ∘F G
-  CatPrecategory .⋆IdL _ = F-lUnit
-  CatPrecategory .⋆IdR _ = F-rUnit
-  CatPrecategory .⋆Assoc _ _ _ = F-assoc
-
--- TODO: what is required for Functor C D to be a set?
-
\ No newline at end of file diff --git a/Cubical.Categories.Instances.TypePrecategory.html b/Cubical.Categories.Instances.TypePrecategory.html deleted file mode 100644 index b7366906eb..0000000000 --- a/Cubical.Categories.Instances.TypePrecategory.html +++ /dev/null @@ -1,21 +0,0 @@ - -Cubical.Categories.Instances.TypePrecategory
{-# OPTIONS --safe #-}
-module Cubical.Categories.Instances.TypePrecategory where
-
-open import Cubical.Foundations.Prelude
-
-open import Cubical.Categories.Category.Precategory
-
-open Precategory
-
--- TYPE precategory has types as objects
-module _ ℓ where
-  TYPE : Precategory (ℓ-suc ℓ) ℓ
-  TYPE .ob           = Type ℓ
-  TYPE .Hom[_,_] A B = A → B
-  TYPE .id           = λ x → x
-  TYPE ._⋆_ f g      = λ x → g (f x)
-  TYPE .⋆IdL f       = refl
-  TYPE .⋆IdR f       = refl
-  TYPE .⋆Assoc f g h = refl
-
\ No newline at end of file diff --git a/Cubical.HITs.Everything.html b/Cubical.HITs.Everything.html index a3c0765d23..64095a1d10 100644 --- a/Cubical.HITs.Everything.html +++ b/Cubical.HITs.Everything.html @@ -54,12 +54,13 @@ import Cubical.HITs.SmashProduct.Hexagon import Cubical.HITs.SmashProduct.Pentagon import Cubical.HITs.SmashProduct.SymmetricMonoidal -import Cubical.HITs.Sn -import Cubical.HITs.Susp -import Cubical.HITs.Susp.LoopAdjunction -import Cubical.HITs.Torus -import Cubical.HITs.Truncation -import Cubical.HITs.TypeQuotients -import Cubical.HITs.UnorderedPair -import Cubical.HITs.Wedge +import Cubical.HITs.SmashProduct.SymmetricMonoidalCat +import Cubical.HITs.Sn +import Cubical.HITs.Susp +import Cubical.HITs.Susp.LoopAdjunction +import Cubical.HITs.Torus +import Cubical.HITs.Truncation +import Cubical.HITs.TypeQuotients +import Cubical.HITs.UnorderedPair +import Cubical.HITs.Wedge \ No newline at end of file diff --git a/Cubical.HITs.SmashProduct.SymmetricMonoidal.html b/Cubical.HITs.SmashProduct.SymmetricMonoidal.html index 4b1a22178e..2d3df66901 100644 --- a/Cubical.HITs.SmashProduct.SymmetricMonoidal.html +++ b/Cubical.HITs.SmashProduct.SymmetricMonoidal.html @@ -1,585 +1,512 @@ Cubical.HITs.SmashProduct.SymmetricMonoidal
{-# OPTIONS --safe #-}
-
-{-
-This file contians a proof that the smash product turns the universe
-of pointed types into a symmetric monoidal precategory. The pentagon
-and hexagon are proved in separate files due to the length of the
-proofs. The remaining identities and the main result are proved here.
--}
-
-module Cubical.HITs.SmashProduct.SymmetricMonoidal where
-
-open import Cubical.HITs.SmashProduct.Base
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Pointed
-open import Cubical.Foundations.Isomorphism
-open import Cubical.HITs.Pushout.Base
-open import Cubical.Data.Unit
-open import Cubical.Data.Sigma
-open import Cubical.HITs.Wedge
-open import Cubical.Foundations.GroupoidLaws
-open import Cubical.Foundations.Pointed.Homogeneous
-open import Cubical.Foundations.Path
-open import Cubical.Foundations.Function
-open import Cubical.Foundations.Equiv
-open import Cubical.HITs.SmashProduct.Base
-open import Cubical.HITs.SmashProduct.Pentagon
-open import Cubical.HITs.SmashProduct.Hexagon
-open import Cubical.Categories.Category.Precategory
-  renaming (_×_ to _×'_)
-open import Cubical.Data.Bool
-
-open Precategory hiding (_∘_)
-open Prefunctor
-open isSymmetricPrecategory
-open isMonoidalPrecategory
-open PreNatIso
-open PreNatTrans
-open preIsIso
-
-
-private
-  variable
-    ℓ ℓ' : Level
-    A B : Pointed ℓ
-
-⋀→∙-idfun : {A : Pointed ℓ} {B : Pointed ℓ'}
-  → (_⋀→∙_ (idfun∙ A) (idfun∙ B)) ≡ idfun∙ (A ⋀∙ B)
-⋀→∙-idfun =
-  ΣPathP (funExt
-    (⋀-fun≡ _ _ refl (λ _ → refl)
-      (λ x → flipSquare (sym (rUnit (push (inl x)))))
-      λ x → flipSquare (sym (rUnit (push (inr x)))))
-                   , refl)
-
-⋀→∙-comp : {A A' A'' B B' B'' : Pointed ℓ}
-  (f : A →∙ A') (f' : A' →∙ A'')
-  (g : B →∙ B') (g' : B' →∙ B'')
-  → ((f' ∘∙ f) ⋀→∙ (g' ∘∙ g)) ≡ ((f' ⋀→∙ g') ∘∙ (f ⋀→∙ g))
-⋀→∙-comp f f' g g' =
-  ΣPathP ((funExt
-   (⋀-fun≡ _ _ refl (λ _ → refl)
-     (λ x → flipSquare
-       (cong (push (inl (fst f' (fst f x))) ∙_)
-         ((λ i j → cong-∙ (λ y → inr (fst f' (fst f x) , y))
-                        (cong (fst g') (snd g)) (snd g') i (~ j))
-        ∙ symDistr (cong (λ y → inr (fst f' (fst f x) , y))
-                          (λ i → fst g' (snd g i)))
-                    (cong (λ y → inr (fst f' (fst f x) , y)) (snd g')))
-       ∙ assoc _ _ _
-       ∙∙ (λ j → (push (inl (fst f' (fst f x)))
-           ∙ (λ j → inr (fst f' (fst f x) , snd g' (~ j))))
-           ∙ λ j → inr (fst f' (f .fst x) , fst g' (snd g (~ j))))
-       ∙∙ sym (cong-∙ (f' ⋀→ g') (push (inl (fst f x)))
-         λ i → inr (fst f x , g .snd (~ i)))))
-     λ x → flipSquare
-       (cong (push (inr (fst g' (fst g x))) ∙_)
-         ((λ i j → cong-∙ (λ y → inr (y , fst g' (fst g x)))
-                        (cong (fst f') (snd f)) (snd f') i (~ j))
-        ∙ symDistr (cong (λ y → inr (y , fst g' (fst g x)))
-                          (λ i → fst f' (snd f i)))
-                    (cong (λ y → inr (y , fst g' (fst g x))) (snd f')))
-       ∙ assoc _ _ _
-       ∙∙ (λ j → (push (inr (fst g' (fst g x)))
-           ∙ (λ j → inr (snd f' (~ j) , fst g' (fst g x))))
-           ∙ λ j → inr (fst f' (snd f (~ j)) , fst g' (g .fst x)))
-       ∙∙ sym (cong-∙ (f' ⋀→ g') (push (inr (fst g x)))
-                  λ i → inr ((snd f (~ i)) , fst g x)))))
-        , (rUnit refl))
-
-⋀assoc-⋀→∙ : {A A' B B' C C' : Pointed ℓ}
-  (f : A →∙ A') (g : B →∙ B') (h : C →∙ C') →
-      ≃∙map SmashAssocEquiv∙ ∘∙ (f ⋀→∙ (g ⋀→∙ h))
-    ≡ ((f ⋀→∙ g) ⋀→∙ h) ∘∙ ≃∙map SmashAssocEquiv∙
-⋀assoc-⋀→∙ {A = A} {A' = A'} {B = B} {B' = B'} {C = C} {C' = C'} f g h =
-  ΣPathP
-   ((funExt (⋀-fun≡'.main _ _
-     (λ x → mainᵣ (fst x) (snd x))
-     (λ x → p≡refl ◁ flipSquare
-       (cong (cong (SmashAssocIso .Iso.fun))
-         (sym (rUnit (push (inl (fst f x))))))
-         ▷ λ _ → refl)
-     (⋀→∙Homogeneous≡ (isHomogeneousPath _ _)
-       λ y z → (λ i → push-lem y z (~ i)
-                    ∙∙ refl
-                    ∙∙ sym (push-lem y z i0))
-           ∙ ∙∙lCancel (sym (push-lem y z i0))
-           ∙ sym p≡refl)))
-  , λ i j → pt-lem-main i j)
-  where
-  mainᵣ : (x : fst A) (y : B ⋀ C)
-    → SmashAssocIso .Iso.fun (inr (fst f x , (g ⋀→ h) y))
-     ≡ ((f ⋀→∙ g) ⋀→ h) (SmashAssocIso .Iso.fun (inr (x , y)))
-  mainᵣ x =
-    ⋀-fun≡ _ _ refl (λ _ → refl)
-      (λ b → flipSquare
-        (cong-∙ (λ z → SmashAssocIso .Iso.fun (inr (fst f x , z)))
-                (push (inl (fst g b)))
-                (λ i₁ → inr (fst g b , snd h (~ i₁)))))
-      λ b → flipSquare
-        (cong-∙ (λ z → SmashAssocIso .Iso.fun (inr (fst f x , z)))
-                (push (inr (fst h b)))
-                (λ i₁ → inr (snd g (~ i₁) , fst h b))
-       ∙∙ cong₂ _∙_ ((λ j i → ⋀CommIso .Iso.fun
-                   (compPath≡compPath'
-                     (push (inl (fst h b)))
-                     (λ i → inr (fst h b , push (inl (fst f x)) i)) (~ j) i))
-                    ∙ cong-∙ (⋀CommIso .Iso.fun)
-                        (push (inl (fst h b)))
-                        λ i → inr (fst h b , push (inl (fst f x)) i))
-                    refl
-        ∙ sym (assoc _ _ _)
-        ∙ cong₂ _∙_ refl (sym (cong-∙ (λ y → (inr (y , fst h b)))
-                                (push (inl (fst f x)))
-                                (λ i₁ → inr (fst f x , snd g (~ i₁)))))
-       ∙∙ sym (lem b))
-     where
-     lem : (b : _) → cong ((f ⋀→∙ g) ⋀→ h)
-             (cong (SmashAssocIso .Iso.fun) λ i → inr (x , push (inr b) i))
-          ≡ (push (inr (fst h b)))
-          ∙ λ i → inr (((push (inl (fst f x))
-          ∙ λ i₁ → inr (fst f x , snd g (~ i₁))) i) , (fst h b))
-     lem b = (λ j i → ((f ⋀→∙ g) ⋀→ h)
-                 (⋀CommIso .Iso.fun
-                   (compPath≡compPath' (push (inl b))
-                     (λ i → inr (b , push (inl x) i)) (~ j) i)))
-           ∙∙ cong-∙ (((f ⋀→∙ g) ⋀→ h) ∘ ⋀CommIso .Iso.fun)
-                (push (inl b)) (λ i → inr (b , push (inl x) i))
-           ∙∙ cong₂ _∙_
-               (sym (rUnit _))
-               refl
-
-  push-lem : (y : _) (z : _)
-    → cong (((f ⋀→∙ g) ⋀→ h) ∘ (fst (fst SmashAssocEquiv∙)))
-            (push (inr (inr (y , z))))
-     ≡ cong (fst (≃∙map SmashAssocEquiv∙ ∘∙ (f ⋀→∙ (g ⋀→∙ h))))
-            (push (inr (inr (y , z))))
-  push-lem y z =
-      cong (cong ((f ⋀→∙ g) ⋀→ h))
-           (cong-∙∙ ⋀comm→ (push (inl z))
-                            (λ i → inr (z , push (inr y) i))
-                            refl
-         ∙ sym (compPath≡compPath' (push (inr z)) _))
-   ∙∙ cong-∙ ((f ⋀→∙ g) ⋀→ h)
-        (push (inr z)) (λ i → inr (push (inr y) i , z))
-   ∙∙ (cong₂ _∙_ (sym (rUnit (push (inr (fst h z)))))
-                 (cong-∙ (λ x → inr (x , fst h z))
-                         (push (inr (fst g y)))
-                         (λ i → inr (snd f (~ i) , fst g y)))
-     ∙ sym (cong-∙ (SmashAssocIso .Iso.fun)
-             (push (inr (inr (fst g y , fst h z))))
-             (λ i → inr (snd f (~ i)
-                        , inr (fst g y , fst h z)))
-        ∙∙ cong (_∙ (λ i → inr (inr (snd f (~ i) , fst g y) , fst h z)))
-                (cong-∙∙ ⋀comm→
-                         (push (inl (fst h z)))
-                         (λ i → inr (fst h z , push (inr (fst g y)) i))
-                         refl
-             ∙ sym (compPath≡compPath' (push (inr (fst h z))) _))
-        ∙∙ sym (assoc _ _ _)))
-
-  module N = ⋀-fun≡'
-      (λ z → SmashAssocIso .Iso.fun ((f ⋀→ (g ⋀→∙ h)) z))
-      (λ z → ((f ⋀→∙ g) ⋀→ h) (SmashAssocIso .Iso.fun z))
-      (λ x₁ → mainᵣ (fst x₁) (snd x₁))
-
-  p≡refl : N.p ≡ refl
-  p≡refl = (λ j → cong (SmashAssocIso .Iso.fun
-                       ∘ ((f ⋀→ (g ⋀→∙ h))))
-                         (push (inr (inl tt)))
-                 ∙∙ refl
-                 ∙∙ cong (((f ⋀→∙ g) ⋀→ h)
-                         ∘ (SmashAssocIso .Iso.fun))
-                         (sym (push (push tt j))))
-          ∙ cong (λ x → x ∙∙ refl ∙∙ refl)
-                  (cong-∙ (SmashAssocIso .Iso.fun)
-                          (push (inr (inl tt)))
-                          (λ i → inr (snd f (~ i) , inl tt))
-                 ∙ sym (rUnit refl))
-          ∙ sym (rUnit refl)
-
-  pt-lem : cong (fst (≃∙map SmashAssocEquiv∙ ∘∙ (f ⋀→∙ (g ⋀→∙ h))))
-             (push (inr (inl tt)))
-         ≡ cong (fst (((f ⋀→∙ g) ⋀→∙ h) ∘∙ ≃∙map SmashAssocEquiv∙))
-             (push (inr (inl tt)))
-  pt-lem i j =
-    fst (≃∙map SmashAssocEquiv∙) (rUnit (push (inr (inl tt))) (~ i) j)
-
-  pt-lem-main : I → I → _
-  pt-lem-main i j =
-    hcomp (λ k → λ {(i = i0) → rUnit (refl {x = inl tt}) k j
-                   ; (i = i1) → rUnit (refl {x = inl tt}) k j
-                   ; (j = i0) → (pt-lem i0 ∙∙ refl ∙∙ sym (pt-lem k)) i
-                   ; (j = i1) → inl tt})
-          (∙∙lCancel (sym (pt-lem i0)) j i)
-
-⋀comm-sq : {A A' B B' : Pointed ℓ}
-  (f : A →∙ A') (g : B →∙ B')
-  → (⋀comm→∙ ∘∙ (f ⋀→∙ g)) ≡ ((g ⋀→∙ f) ∘∙ ⋀comm→∙)
-⋀comm-sq f g =
-  ΣPathP ((funExt
-    (⋀-fun≡ _ _ refl (λ _ → refl)
-      (λ x → flipSquare
-        (cong-∙ ⋀comm→
-          (push (inl (fst f x))) (λ i → inr (fst f x , snd g (~ i)))))
-      λ b → flipSquare (cong-∙ ⋀comm→
-                         (push (inr (fst g b)))
-                         (λ i → inr (snd f (~ i) , fst g b)))))
-    , refl)
-
-⋀comm-sq' : {A A' B B' : Pointed ℓ}
-  (f : A →∙ A') (g : B →∙ B')
-  → (f ⋀→∙ g) ≡ (⋀comm→∙ ∘∙ ((g ⋀→∙ f) ∘∙ ⋀comm→∙))
-⋀comm-sq' f g =
-     sym (∘∙-idʳ (f ⋀→∙ g))
-  ∙∙ cong (_∘∙ (f ⋀→∙ g)) (sym lem)
-  ∙∙ ∘∙-assoc ⋀comm→∙ ⋀comm→∙ (f ⋀→∙ g)
-   ∙ cong (λ w → ⋀comm→∙ ∘∙ w) (⋀comm-sq f g)
-  where
-  lem : ⋀comm→∙ ∘∙ ⋀comm→∙ ≡ idfun∙ _
-  lem = ΣPathP ((funExt (Iso.rightInv ⋀CommIso)) , (sym (rUnit refl)))
-
-Bool⋀→ : Bool*∙ {ℓ} ⋀ A → typ A
-Bool⋀→ {A = A} (inl x) = pt A
-Bool⋀→ (inr (lift false , a)) = a
-Bool⋀→ {A = A} (inr (lift true , a)) = pt A
-Bool⋀→ {A = A} (push (inl (lift false)) i) = pt A
-Bool⋀→ {A = A} (push (inl (lift true)) i) = pt A
-Bool⋀→ {A = A} (push (inr x) i) = pt A
-Bool⋀→ {A = A} (push (push a i₁) i) = pt A
-
-⋀lIdIso : Iso (Bool*∙ {ℓ} ⋀ A) (typ A)
-Iso.fun (⋀lIdIso {A = A}) (inl x) = pt A
-Iso.fun ⋀lIdIso = Bool⋀→
-Iso.inv ⋀lIdIso a = inr (false* , a)
-Iso.rightInv ⋀lIdIso a = refl
-Iso.leftInv (⋀lIdIso {A = A}) =
-  ⋀-fun≡ _ _ (sym (push (inl false*))) h hₗ
-    λ x → compPath-filler (sym (push (inl false*))) (push (inr x))
-  where
-  h : (x : (Lift Bool) × fst A) →
-      inr (false* , Bool⋀→ (inr x)) ≡ inr x
-  h (lift false , a) = refl
-  h (lift true , a) = sym (push (inl false*)) ∙ push (inr a)
-
-  hₗ : (x : Lift Bool) →
-      PathP
-      (λ i → inr (false* , Bool⋀→ (push (inl x) i)) ≡ push (inl x) i)
-      (λ i → push (inl false*) (~ i)) (h (x , pt A))
-  hₗ (lift false) i j = push (inl false*) (~ j ∨ i)
-  hₗ (lift true) =
-      compPath-filler (sym (push (inl false*))) (push (inl true*))
-    ▷ (cong (sym (push (inl false*)) ∙_)
-       λ j i → push (push tt j) i)
-
-⋀lIdEquiv∙ : Bool*∙ {ℓ} ⋀∙ A ≃∙ A
-fst ⋀lIdEquiv∙ = isoToEquiv ⋀lIdIso
-snd ⋀lIdEquiv∙ = refl
-
-⋀lId-sq : (f : A →∙ B) →
-      (≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ (idfun∙ Bool*∙ ⋀→∙ f))
-    ≡ (f ∘∙ ≃∙map ⋀lIdEquiv∙)
-⋀lId-sq {ℓ} {A = A} {B = B} f =
-  ΣPathP ((funExt
-    (⋀-fun≡ _ _ (sym (snd f)) (λ x → h (fst x) (snd x)) hₗ hᵣ))
-  , (sym (rUnit refl) ◁ (λ i j → snd f (~ i ∨ j))
-    ▷ lUnit (snd f)))
-  where
-  h : (x : Lift Bool) (a : fst A)
-    → Bool⋀→ (inr (x , fst f a)) ≡ fst f (Bool⋀→ (inr (x , a)))
-  h (lift false) a = refl
-  h (lift true) a = sym (snd f)
-
-  hₗ : (x : Lift Bool)
-    → PathP (λ i → Bool⋀→ ((idfun∙ Bool*∙ ⋀→ f) (push (inl x) i))
-                   ≡ fst f (Bool⋀→ (push (inl x) i)))
-             (sym (snd f)) (h x (pt A))
-  hₗ (lift false) =
-    flipSquare ((cong-∙ (Bool⋀→ {ℓ})
-                  (push (inl false*))
-                  (λ i → inr (lift false , snd f (~ i)))
-              ∙ sym (lUnit (sym (snd f))))
-             ◁ λ i j → snd f (~ i ∧ ~ j))
-  hₗ (lift true) =
-    flipSquare
-       ((cong-∙ (Bool⋀→ {ℓ})
-         (push (inl true*)) (λ i → inr (lift true , snd f (~ i)))
-       ∙ sym (rUnit refl))
-      ◁ λ i _ → snd f (~ i))
-
-  hᵣ : (x : fst A)
-    → PathP (λ i → Bool⋀→ {ℓ} ((idfun∙ Bool*∙ ⋀→ f) (push (inr x) i))
-                   ≡ fst f (snd A))
-             (sym (snd f)) (h true* x)
-  hᵣ x = flipSquare ((cong-∙ (Bool⋀→ {ℓ})
-                      (push (inr (fst f x)))
-                      (λ i → inr (true* , fst f x))
-                    ∙ sym (rUnit refl))
-      ◁ λ i _ → snd f (~ i))
-
-⋀lId-assoc : ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→∙ idfun∙ B)
-             ∘∙ ≃∙map SmashAssocEquiv∙)
-            ≡ ≃∙map ⋀lIdEquiv∙
-⋀lId-assoc {ℓ} {A = A} {B = B} =
-  ΣPathP (funExt
-          (⋀-fun≡'.main _ _
-            (λ xy → mainᵣ (fst xy) (snd xy))
-            (λ x → sym (rUnit refl) ◁ mainᵣ-pt-coh x)
-            (⋀→∙Homogeneous≡ (isHomogeneousPath _ _) mainᵣ-coh))
-        , (sym (rUnit refl)
-          ◁ flipSquare (sym (rUnit refl))))
-  where
-  l₁ : (x : Lift Bool) → inl tt ≡ Bool⋀→ (inr (x , inl tt))
-  l₁ (lift true) = refl
-  l₁ (lift false) = refl
-
-  l₂ : (x : Lift Bool) (y : fst A × fst B)
-    → inr (Bool⋀→ (inr (x , fst y)) , snd y)
-    ≡ Bool⋀→ (inr (x , inr y))
-  l₂ (lift true) y = sym (push (inr (snd y)))
-  l₂ (lift false) y = refl
-
-  l₁≡l₂-left : (x : Lift Bool) (y : fst A) →
-    PathP (λ i → l₁ x i ≡ l₂ x (y , pt B) i)
-          (push (inl (Bool⋀→ (inr (x , y)))))
-          λ i → Bool⋀→ {ℓ} {A = A ⋀∙ B} (inr (x , push (inl y) i))
-  l₁≡l₂-left (lift true) y = (λ i → push (push tt i))
-                   ◁ λ i j → push (inr (pt B)) (~ i ∧ j)
-  l₁≡l₂-left (lift false) y = refl
-
-  l₁≡l₂-right : (x : Lift Bool) (y : fst B)
-    → PathP (λ i → l₁ x i ≡ l₂ x ((pt A) , y) i)
-            (push (inr y) ∙ (λ i → inr (Bool⋀→ {A = A} (push (inl x) i) , y)))
-            (λ i → Bool⋀→ {A = A ⋀∙ B} (inr (x , push (inr y) i)))
-  l₁≡l₂-right (lift false) y = sym (rUnit (push (inr y)))
-  l₁≡l₂-right (lift true) y = sym (rUnit (push (inr y)))
-                   ◁ λ i j → push (inr y) (j ∧ ~ i)
-
-  mainᵣ : (x : Lift Bool) (y : A ⋀ B)
-    → (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B)
-        (SmashAssocIso .Iso.fun (inr (x , y)))
-     ≡ Bool⋀→ {ℓ} (inr (x , y))
-  mainᵣ x = ⋀-fun≡ _ _ (l₁ x) (l₂ x)
-    (λ y → flipSquare (sym (rUnit (push (inl (Bool⋀→ (inr (x , y))))))
-          ◁ l₁≡l₂-left x y))
-    λ y → flipSquare (
-      (cong (cong (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B))
-            (cong-∙∙ ⋀comm→
-              (push (inl y)) (λ i → inr (y , push (inl x) i)) refl
-          ∙ sym (compPath≡compPath'
-                  (push (inr y)) (λ i → inr (push (inl x) i , y))))
-        ∙ cong-∙ (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B)
-            (push (inr y)) λ i → inr (push (inl x) i , y))
-        ◁ (cong₂ _∙_ (sym (rUnit (push (inr y))))
-                     refl
-                   ◁ l₁≡l₂-right x y))
-
-  mainᵣ-pt-coh : (x : Lift Bool)
-    → PathP (λ i → inl tt ≡ Bool⋀→ (push (inl x) i))
-             refl (mainᵣ x (inl tt))
-  mainᵣ-pt-coh (lift false) = refl
-  mainᵣ-pt-coh (lift true) = refl
-
-  module N = ⋀-fun≡'
-    (λ z → (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B) (SmashAssocIso .Iso.fun z))
-    (λ z → ⋀lIdIso .Iso.fun z)
-    (λ xy → mainᵣ (fst xy) (snd xy))
-  open N
-
-  lem : (x : fst A) (y : fst B)
-    → cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→ idfun∙ B)
-            ∘ SmashAssocIso .Iso.fun)
-             (push (inr (inr (x , y))))
-    ≡ push (inr y)
-  lem x y =
-      cong (cong (≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→ idfun∙ B))
-            (cong-∙∙ ⋀comm→
-              (push (inl y)) (λ i → inr (y , push (inr x) i)) refl
-           ∙ sym (compPath≡compPath'
-                  (push (inr y)) λ i → inr (push (inr x) i , y)))
-    ∙∙ cong-∙ (≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→ idfun∙ B)
-              (push (inr y))
-              (λ i → inr (push (inr x) i , y))
-    ∙∙ (sym (rUnit _)
-     ∙ sym (rUnit _))
-
-  mainᵣ-coh : (x : fst A) (y : fst B)
-    → Fₗ .fst (inr (x , y)) ≡ Fᵣ .fst (inr (x , y))
-  mainᵣ-coh x y =
-      (λ i → lem x y i ∙∙ sym (lem x y i1) ∙∙ refl)
-    ∙ sym (compPath≡compPath'
-           (push (inr y)) (sym (push (inr y))))
-    ∙ rCancel (push (inr y))
-    ∙ rUnit refl
-
--- Triangle equality
-⋀triang : ∀ {ℓ} {A B : Pointed ℓ}
-  → (((≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ ⋀comm→∙) ⋀→∙ idfun∙ B)
-    ∘∙ ≃∙map SmashAssocEquiv∙)
-    ≡ idfun∙ A ⋀→∙ ≃∙map (⋀lIdEquiv∙ {ℓ} {A = B})
-⋀triang {ℓ = ℓ} {A = A} {B = B} =
-  ΣPathP ((funExt (⋀-fun≡'.main _ _
-    (λ x → mainᵣ (fst x) (snd x))
-    (λ x → p≡refl
-         ◁ flipSquare ((λ i j → push (inl x) (i ∧ j))
-         ▷ rUnit (push (inl x))))
-    (⋀→∙Homogeneous≡ (isHomogeneousPath _ _)
-      λ x y → Fₗ≡refl x y ∙ sym (Fᵣ≡refl x y))))
-    , (sym (rUnit refl) ◁ flipSquare p≡refl))
-  where
-  mainᵣ-hom : (x : fst A) (y : Bool* {ℓ}) (z : fst B)
-    → Path (A ⋀ B) (inr (Bool⋀→ (inr (y , x)) , z))
-                    (inr (x , Bool⋀→ (inr (y , z))))
-  mainᵣ-hom x (lift false) z = refl
-  mainᵣ-hom x (lift true) z = sym (push (inr z)) ∙ push (inl x)
-
-  mainᵣ : (x : fst A) (y : Bool*∙ {ℓ} ⋀ B) →
-    ((≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ ⋀comm→∙) ⋀→ (idfun∙ B))
-      (Iso.fun (SmashAssocIso {A = A} {B = Bool*∙ {ℓ}} {C = B}) (inr (x , y)))
-    ≡ inr (x , ⋀lIdIso .Iso.fun y)
-  mainᵣ x = ⋀-fun≡ _ _ (push (inl x))
-    (λ y → mainᵣ-hom x (fst y) (snd y))
-    (λ { (lift false) → flipSquare (sym (rUnit (push (inl x)))
-                       ◁ λ i j → push (inl x) (j ∨ i))
-       ; (lift true) → flipSquare ((sym (rUnit (push (inl (pt A))))
-                                   ∙ λ j i → push (push tt j) i)
-                     ◁ λ i j → compPath-filler'
-                                 (sym (push (inr (pt B)))) (push (inl x)) j i)})
-     λ b → flipSquare
-       ((cong (cong (((≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)))
-         (cong-∙∙ ⋀comm→ (push (inl b)) (λ i → inr (b , push (inl x) i)) refl
-         ∙ sym (compPath≡compPath'
-                 (push (inr b)) (λ i → inr (push (inl x) i , b))))
-       ∙ cong-∙ (((≃∙map (⋀lIdEquiv∙ {ℓ})  ∘∙ ⋀comm→∙) ⋀→ idfun∙ B))
-                (push (inr b)) (λ i → inr (push (inl x) i , b))
-       ∙ sym (rUnit _)
-       ∙ (λ i → (push (inr b) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , b))))
-       ∙ sym (rUnit (push (inr b))))
-       ◁ λ i j → compPath-filler' (sym (push (inr b))) (push (inl x)) j i)
-
-  lemₗ : cong (idfun∙ A ⋀→ ≃∙map (⋀lIdEquiv∙ {ℓ} {A = B}))
-             (push (inr (inl tt)))
-      ≡ (push (inl (snd A)))
-  lemₗ = sym (rUnit _) ∙ λ i → push (push tt (~ i))
-
-  module K = ⋀-fun≡' (λ z →
-          ((≃∙map ⋀lIdEquiv∙ ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
-          (SmashAssocIso .Iso.fun z))
-       (λ z → (idfun∙ A ⋀→ ≃∙map ⋀lIdEquiv∙) z)
-       (λ x₁ → mainᵣ (fst x₁) (snd x₁))
-  open K
-
-  p≡refl : p ≡ refl
-  p≡refl = cong (push (inl (snd A)) ∙_) (cong sym lemₗ)
-         ∙ rCancel (push (inl (pt A)))
-
-  Fₗ-false : (y : fst B)
-    → cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
-        (cong ⋀comm→ (push (inl y)
-                   ∙' (λ i → inr (y , push (inr (lift false)) i))))
-      ≡ push (inr y)
-  Fₗ-false y =
-      cong (cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B))
-         (cong (cong ⋀comm→)
-           (sym (compPath≡compPath'
-             (push (inl y)) (λ i → inr (y , push (inr (lift false)) i))))
-       ∙ cong-∙ ⋀comm→ (push (inl y))
-                        (λ i → inr (y , push (inr (lift false)) i)))
-    ∙∙ cong-∙ ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
-              (push (inr y)) (λ i → inr (push (inr (lift false)) i , y))
-    ∙∙ (sym (rUnit _)
-     ∙ (λ i → push (inr y) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , y)))
-     ∙ sym (rUnit _))
-
-  Fₗ-true : (y : fst B)
-    → cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
-        (cong (SmashAssocIso .Iso.fun) (push (inr (inr (lift true , y)))))
-      ≡ push (inr y)
-  Fₗ-true y =
-      cong (cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B))
-        (cong-∙∙ ⋀comm→ (push (inl y)) (λ i → inr (y , push (inr true*) i)) refl
-        ∙ sym (compPath≡compPath' (push (inr y))
-                                  λ i → inr (push (inr true*) i , y)))
-    ∙∙ cong-∙ ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
-              (push (inr y))
-              (λ i → inr (push (inr true*) i , y))
-    ∙∙ ((sym (rUnit _)
-     ∙ (λ i → push (inr y) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , y)))
-     ∙ sym (rUnit _)))
-
-  Fₗ≡refl : (x : Lift Bool) (y : fst B) → Fₗ .fst (inr (x , y)) ≡ refl
-  Fₗ≡refl (lift false) y =
-     (λ i → Fₗ-false y i ∙∙ refl ∙∙ sym (rUnit (push (inr y)) (~ i)))
-    ∙ ∙∙lCancel _
-  Fₗ≡refl (lift true) y =
-      (λ j → Fₗ-true y j
-          ∙∙ (sym (push (inr y)) ∙ push (push tt j))
-          ∙∙ sym (rUnit (push (inr (pt B))) (~ j)))
-    ∙ (λ j → (λ i → push (inr y) (i ∧ ~ j))
-           ∙∙ (λ i → push (inr y) (~ j ∧ ~ i))
-            ∙ push (inr (pt B))
-           ∙∙ sym (push (inr (pt B))))
-    ∙ cong (_∙ sym (push (inr (pt B)))) (sym (lUnit (push (inr (pt B)))))
-    ∙ rCancel _
-
-  Fᵣ≡refl : (x : Lift Bool) (y : fst B) → Fᵣ .fst (inr (x , y)) ≡ refl
-  Fᵣ≡refl x y =
-    cong (push (inl (snd A)) ∙_)
-      (sym (rUnit _) ∙ (λ i j → push (push tt (~ i)) (~ j)))
-    ∙ rCancel _
-
-
--- ⋀ as a functor
-⋀F : ∀ {ℓ} → Prefunctor (PointedCat ℓ ×' PointedCat ℓ) (PointedCat ℓ)
-F-ob ⋀F (A , B) = A ⋀∙ B
-F-hom ⋀F (f , g) = f ⋀→∙ g
-F-id ⋀F = ⋀→∙-idfun
-F-seq ⋀F (f , g) (f' , g') = ⋀→∙-comp f f' g g'
-
-⋀lUnitNatIso : PreNatIso (PointedCat ℓ) (PointedCat ℓ)
-      (restrFunctorₗ ⋀F Bool*∙) (idPrefunctor (PointedCat ℓ))
-N-ob (trans ⋀lUnitNatIso) X = ≃∙map ⋀lIdEquiv∙
-N-hom (trans ⋀lUnitNatIso) f = ⋀lId-sq f
-inv' (isIs ⋀lUnitNatIso c) = ≃∙map (invEquiv∙ ⋀lIdEquiv∙)
-sect (isIs (⋀lUnitNatIso {ℓ = ℓ}) c) =
-  ≃∙→ret/sec∙ (⋀lIdEquiv∙ {ℓ = ℓ} {A = c}) .snd
-retr (isIs ⋀lUnitNatIso c) =
-  ≃∙→ret/sec∙ ⋀lIdEquiv∙ .fst
-
-makeIsIso-Pointed : ∀ {ℓ} {A B : Pointed ℓ} {f : A →∙ B}
-  → isEquiv (fst f) → preIsIso {C = PointedCat ℓ} f
-inv' (makeIsIso-Pointed {f = f} eq) = ≃∙map (invEquiv∙ ((fst f , eq) , snd f))
-sect (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f)  .snd
-retr (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f)  .fst
-
-restrₗᵣ : PreNatIso (PointedCat ℓ) (PointedCat ℓ)
-      (restrFunctorᵣ ⋀F Bool*∙) (restrFunctorₗ ⋀F Bool*∙)
-N-ob (trans restrₗᵣ) X = ⋀comm→∙
-N-hom (trans restrₗᵣ) f = ⋀comm-sq f (idfun∙ Bool*∙)
-isIs restrₗᵣ c = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso)
-
--- main result
-⋀Symm : ∀ {ℓ} → isSymmetricPrecategory (PointedCat ℓ)
-_⊗_ (isMonoidal ⋀Symm) = ⋀F
-𝟙 (isMonoidal ⋀Symm) = Bool*∙
-N-ob (trans (⊗assoc (isMonoidal ⋀Symm))) (A , B , C) = ≃∙map SmashAssocEquiv∙
-N-hom (trans (⊗assoc (isMonoidal ⋀Symm))) (f , g , h) = ⋀assoc-⋀→∙ f g h
-inv' (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) =
-  ≃∙map (invEquiv∙ SmashAssocEquiv∙)
-sect (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) =
-  ≃∙→ret/sec∙ SmashAssocEquiv∙ .snd
-retr (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) =
-  ≃∙→ret/sec∙ SmashAssocEquiv∙ .fst
-⊗lUnit (isMonoidal ⋀Symm) = ⋀lUnitNatIso
-⊗rUnit (isMonoidal ⋀Symm) = compPreNatIso _ _ _ restrₗᵣ ⋀lUnitNatIso
-triang (isMonoidal (⋀Symm {ℓ})) X Y = ⋀triang
-⊗pentagon (isMonoidal ⋀Symm) X Y Z W =
-  (∘∙-assoc assc₅∙ assc₄∙ assc₃∙) ∙ pentagon∙
-N-ob (trans (Braid ⋀Symm)) X = ⋀comm→∙
-N-hom (trans (Braid ⋀Symm)) (f , g) = ⋀comm-sq f g
-isIs (Braid ⋀Symm) _ = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso)
-isSymmetricPrecategory.hexagon ⋀Symm a b c = hexagon∙
-symBraiding ⋀Symm X Y =
-  ΣPathP ((funExt (Iso.rightInv ⋀CommIso)) , (sym (rUnit refl)))
+module Cubical.HITs.SmashProduct.SymmetricMonoidal where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Pointed.Homogeneous
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Sigma
+open import Cubical.Data.Bool
+open import Cubical.HITs.Wedge
+open import Cubical.HITs.Pushout.Base
+open import Cubical.HITs.SmashProduct.Base
+open import Cubical.HITs.SmashProduct.Pentagon
+open import Cubical.HITs.SmashProduct.Hexagon
+
+private
+  variable
+    ℓ ℓ' : Level
+    A B : Pointed ℓ
+
+⋀→∙-idfun : {A : Pointed ℓ} {B : Pointed ℓ'}
+  → (_⋀→∙_ (idfun∙ A) (idfun∙ B)) ≡ idfun∙ (A ⋀∙ B)
+⋀→∙-idfun =
+  ΣPathP (funExt
+    (⋀-fun≡ _ _ refl (λ _ → refl)
+      (λ x → flipSquare (sym (rUnit (push (inl x)))))
+      λ x → flipSquare (sym (rUnit (push (inr x)))))
+                   , refl)
+
+⋀→∙-comp : {A A' A'' B B' B'' : Pointed ℓ}
+  (f : A →∙ A') (f' : A' →∙ A'')
+  (g : B →∙ B') (g' : B' →∙ B'')
+  → ((f' ∘∙ f) ⋀→∙ (g' ∘∙ g)) ≡ ((f' ⋀→∙ g') ∘∙ (f ⋀→∙ g))
+⋀→∙-comp f f' g g' =
+  ΣPathP ((funExt
+   (⋀-fun≡ _ _ refl (λ _ → refl)
+     (λ x → flipSquare
+       (cong (push (inl (fst f' (fst f x))) ∙_)
+         ((λ i j → cong-∙ (λ y → inr (fst f' (fst f x) , y))
+                        (cong (fst g') (snd g)) (snd g') i (~ j))
+        ∙ symDistr (cong (λ y → inr (fst f' (fst f x) , y))
+                          (λ i → fst g' (snd g i)))
+                    (cong (λ y → inr (fst f' (fst f x) , y)) (snd g')))
+       ∙ assoc _ _ _
+       ∙∙ (λ j → (push (inl (fst f' (fst f x)))
+           ∙ (λ j → inr (fst f' (fst f x) , snd g' (~ j))))
+           ∙ λ j → inr (fst f' (f .fst x) , fst g' (snd g (~ j))))
+       ∙∙ sym (cong-∙ (f' ⋀→ g') (push (inl (fst f x)))
+         λ i → inr (fst f x , g .snd (~ i)))))
+     λ x → flipSquare
+       (cong (push (inr (fst g' (fst g x))) ∙_)
+         ((λ i j → cong-∙ (λ y → inr (y , fst g' (fst g x)))
+                        (cong (fst f') (snd f)) (snd f') i (~ j))
+        ∙ symDistr (cong (λ y → inr (y , fst g' (fst g x)))
+                          (λ i → fst f' (snd f i)))
+                    (cong (λ y → inr (y , fst g' (fst g x))) (snd f')))
+       ∙ assoc _ _ _
+       ∙∙ (λ j → (push (inr (fst g' (fst g x)))
+           ∙ (λ j → inr (snd f' (~ j) , fst g' (fst g x))))
+           ∙ λ j → inr (fst f' (snd f (~ j)) , fst g' (g .fst x)))
+       ∙∙ sym (cong-∙ (f' ⋀→ g') (push (inr (fst g x)))
+                  λ i → inr ((snd f (~ i)) , fst g x)))))
+        , (rUnit refl))
+
+⋀assoc-⋀→∙ : {A A' B B' C C' : Pointed ℓ}
+  (f : A →∙ A') (g : B →∙ B') (h : C →∙ C') →
+      ≃∙map SmashAssocEquiv∙ ∘∙ (f ⋀→∙ (g ⋀→∙ h))
+    ≡ ((f ⋀→∙ g) ⋀→∙ h) ∘∙ ≃∙map SmashAssocEquiv∙
+⋀assoc-⋀→∙ {A = A} {A' = A'} {B = B} {B' = B'} {C = C} {C' = C'} f g h =
+  ΣPathP
+   ((funExt (⋀-fun≡'.main _ _
+     (λ x → mainᵣ (fst x) (snd x))
+     (λ x → p≡refl ◁ flipSquare
+       (cong (cong (SmashAssocIso .Iso.fun))
+         (sym (rUnit (push (inl (fst f x))))))
+         ▷ λ _ → refl)
+     (⋀→∙Homogeneous≡ (isHomogeneousPath _ _)
+       λ y z → (λ i → push-lem y z (~ i)
+                    ∙∙ refl
+                    ∙∙ sym (push-lem y z i0))
+           ∙ ∙∙lCancel (sym (push-lem y z i0))
+           ∙ sym p≡refl)))
+  , λ i j → pt-lem-main i j)
+  where
+  mainᵣ : (x : fst A) (y : B ⋀ C)
+    → SmashAssocIso .Iso.fun (inr (fst f x , (g ⋀→ h) y))
+     ≡ ((f ⋀→∙ g) ⋀→ h) (SmashAssocIso .Iso.fun (inr (x , y)))
+  mainᵣ x =
+    ⋀-fun≡ _ _ refl (λ _ → refl)
+      (λ b → flipSquare
+        (cong-∙ (λ z → SmashAssocIso .Iso.fun (inr (fst f x , z)))
+                (push (inl (fst g b)))
+                (λ i₁ → inr (fst g b , snd h (~ i₁)))))
+      λ b → flipSquare
+        (cong-∙ (λ z → SmashAssocIso .Iso.fun (inr (fst f x , z)))
+                (push (inr (fst h b)))
+                (λ i₁ → inr (snd g (~ i₁) , fst h b))
+       ∙∙ cong₂ _∙_ ((λ j i → ⋀CommIso .Iso.fun
+                   (compPath≡compPath'
+                     (push (inl (fst h b)))
+                     (λ i → inr (fst h b , push (inl (fst f x)) i)) (~ j) i))
+                    ∙ cong-∙ (⋀CommIso .Iso.fun)
+                        (push (inl (fst h b)))
+                        λ i → inr (fst h b , push (inl (fst f x)) i))
+                    refl
+        ∙ sym (assoc _ _ _)
+        ∙ cong₂ _∙_ refl (sym (cong-∙ (λ y → (inr (y , fst h b)))
+                                (push (inl (fst f x)))
+                                (λ i₁ → inr (fst f x , snd g (~ i₁)))))
+       ∙∙ sym (lem b))
+     where
+     lem : (b : _) → cong ((f ⋀→∙ g) ⋀→ h)
+             (cong (SmashAssocIso .Iso.fun) λ i → inr (x , push (inr b) i))
+          ≡ (push (inr (fst h b)))
+          ∙ λ i → inr (((push (inl (fst f x))
+          ∙ λ i₁ → inr (fst f x , snd g (~ i₁))) i) , (fst h b))
+     lem b = (λ j i → ((f ⋀→∙ g) ⋀→ h)
+                 (⋀CommIso .Iso.fun
+                   (compPath≡compPath' (push (inl b))
+                     (λ i → inr (b , push (inl x) i)) (~ j) i)))
+           ∙∙ cong-∙ (((f ⋀→∙ g) ⋀→ h) ∘ ⋀CommIso .Iso.fun)
+                (push (inl b)) (λ i → inr (b , push (inl x) i))
+           ∙∙ cong₂ _∙_
+               (sym (rUnit _))
+               refl
+
+  push-lem : (y : _) (z : _)
+    → cong (((f ⋀→∙ g) ⋀→ h) ∘ (fst (fst SmashAssocEquiv∙)))
+            (push (inr (inr (y , z))))
+     ≡ cong (fst (≃∙map SmashAssocEquiv∙ ∘∙ (f ⋀→∙ (g ⋀→∙ h))))
+            (push (inr (inr (y , z))))
+  push-lem y z =
+      cong (cong ((f ⋀→∙ g) ⋀→ h))
+           (cong-∙∙ ⋀comm→ (push (inl z))
+                            (λ i → inr (z , push (inr y) i))
+                            refl
+         ∙ sym (compPath≡compPath' (push (inr z)) _))
+   ∙∙ cong-∙ ((f ⋀→∙ g) ⋀→ h)
+        (push (inr z)) (λ i → inr (push (inr y) i , z))
+   ∙∙ (cong₂ _∙_ (sym (rUnit (push (inr (fst h z)))))
+                 (cong-∙ (λ x → inr (x , fst h z))
+                         (push (inr (fst g y)))
+                         (λ i → inr (snd f (~ i) , fst g y)))
+     ∙ sym (cong-∙ (SmashAssocIso .Iso.fun)
+             (push (inr (inr (fst g y , fst h z))))
+             (λ i → inr (snd f (~ i)
+                        , inr (fst g y , fst h z)))
+        ∙∙ cong (_∙ (λ i → inr (inr (snd f (~ i) , fst g y) , fst h z)))
+                (cong-∙∙ ⋀comm→
+                         (push (inl (fst h z)))
+                         (λ i → inr (fst h z , push (inr (fst g y)) i))
+                         refl
+             ∙ sym (compPath≡compPath' (push (inr (fst h z))) _))
+        ∙∙ sym (assoc _ _ _)))
+
+  module N = ⋀-fun≡'
+      (λ z → SmashAssocIso .Iso.fun ((f ⋀→ (g ⋀→∙ h)) z))
+      (λ z → ((f ⋀→∙ g) ⋀→ h) (SmashAssocIso .Iso.fun z))
+      (λ x₁ → mainᵣ (fst x₁) (snd x₁))
+
+  p≡refl : N.p ≡ refl
+  p≡refl = (λ j → cong (SmashAssocIso .Iso.fun
+                       ∘ ((f ⋀→ (g ⋀→∙ h))))
+                         (push (inr (inl tt)))
+                 ∙∙ refl
+                 ∙∙ cong (((f ⋀→∙ g) ⋀→ h)
+                         ∘ (SmashAssocIso .Iso.fun))
+                         (sym (push (push tt j))))
+          ∙ cong (λ x → x ∙∙ refl ∙∙ refl)
+                  (cong-∙ (SmashAssocIso .Iso.fun)
+                          (push (inr (inl tt)))
+                          (λ i → inr (snd f (~ i) , inl tt))
+                 ∙ sym (rUnit refl))
+          ∙ sym (rUnit refl)
+
+  pt-lem : cong (fst (≃∙map SmashAssocEquiv∙ ∘∙ (f ⋀→∙ (g ⋀→∙ h))))
+             (push (inr (inl tt)))
+         ≡ cong (fst (((f ⋀→∙ g) ⋀→∙ h) ∘∙ ≃∙map SmashAssocEquiv∙))
+             (push (inr (inl tt)))
+  pt-lem i j =
+    fst (≃∙map SmashAssocEquiv∙) (rUnit (push (inr (inl tt))) (~ i) j)
+
+  pt-lem-main : I → I → _
+  pt-lem-main i j =
+    hcomp (λ k → λ {(i = i0) → rUnit (refl {x = inl tt}) k j
+                   ; (i = i1) → rUnit (refl {x = inl tt}) k j
+                   ; (j = i0) → (pt-lem i0 ∙∙ refl ∙∙ sym (pt-lem k)) i
+                   ; (j = i1) → inl tt})
+          (∙∙lCancel (sym (pt-lem i0)) j i)
+
+⋀comm-sq : {A A' B B' : Pointed ℓ}
+  (f : A →∙ A') (g : B →∙ B')
+  → (⋀comm→∙ ∘∙ (f ⋀→∙ g)) ≡ ((g ⋀→∙ f) ∘∙ ⋀comm→∙)
+⋀comm-sq f g =
+  ΣPathP ((funExt
+    (⋀-fun≡ _ _ refl (λ _ → refl)
+      (λ x → flipSquare
+        (cong-∙ ⋀comm→
+          (push (inl (fst f x))) (λ i → inr (fst f x , snd g (~ i)))))
+      λ b → flipSquare (cong-∙ ⋀comm→
+                         (push (inr (fst g b)))
+                         (λ i → inr (snd f (~ i) , fst g b)))))
+    , refl)
+
+⋀comm-sq' : {A A' B B' : Pointed ℓ}
+  (f : A →∙ A') (g : B →∙ B')
+  → (f ⋀→∙ g) ≡ (⋀comm→∙ ∘∙ ((g ⋀→∙ f) ∘∙ ⋀comm→∙))
+⋀comm-sq' f g =
+     sym (∘∙-idʳ (f ⋀→∙ g))
+  ∙∙ cong (_∘∙ (f ⋀→∙ g)) (sym lem)
+  ∙∙ ∘∙-assoc ⋀comm→∙ ⋀comm→∙ (f ⋀→∙ g)
+   ∙ cong (λ w → ⋀comm→∙ ∘∙ w) (⋀comm-sq f g)
+  where
+  lem : ⋀comm→∙ ∘∙ ⋀comm→∙ ≡ idfun∙ _
+  lem = ΣPathP ((funExt (Iso.rightInv ⋀CommIso)) , (sym (rUnit refl)))
+
+Bool⋀→ : Bool*∙ {ℓ} ⋀ A → typ A
+Bool⋀→ {A = A} (inl x) = pt A
+Bool⋀→ (inr (lift false , a)) = a
+Bool⋀→ {A = A} (inr (lift true , a)) = pt A
+Bool⋀→ {A = A} (push (inl (lift false)) i) = pt A
+Bool⋀→ {A = A} (push (inl (lift true)) i) = pt A
+Bool⋀→ {A = A} (push (inr x) i) = pt A
+Bool⋀→ {A = A} (push (push a i₁) i) = pt A
+
+⋀lIdIso : Iso (Bool*∙ {ℓ} ⋀ A) (typ A)
+Iso.fun (⋀lIdIso {A = A}) (inl x) = pt A
+Iso.fun ⋀lIdIso = Bool⋀→
+Iso.inv ⋀lIdIso a = inr (false* , a)
+Iso.rightInv ⋀lIdIso a = refl
+Iso.leftInv (⋀lIdIso {A = A}) =
+  ⋀-fun≡ _ _ (sym (push (inl false*))) h hₗ
+    λ x → compPath-filler (sym (push (inl false*))) (push (inr x))
+  where
+  h : (x : (Lift Bool) × fst A) →
+      inr (false* , Bool⋀→ (inr x)) ≡ inr x
+  h (lift false , a) = refl
+  h (lift true , a) = sym (push (inl false*)) ∙ push (inr a)
+
+  hₗ : (x : Lift Bool) →
+      PathP
+      (λ i → inr (false* , Bool⋀→ (push (inl x) i)) ≡ push (inl x) i)
+      (λ i → push (inl false*) (~ i)) (h (x , pt A))
+  hₗ (lift false) i j = push (inl false*) (~ j ∨ i)
+  hₗ (lift true) =
+      compPath-filler (sym (push (inl false*))) (push (inl true*))
+    ▷ (cong (sym (push (inl false*)) ∙_)
+       λ j i → push (push tt j) i)
+
+⋀lIdEquiv∙ : Bool*∙ {ℓ} ⋀∙ A ≃∙ A
+fst ⋀lIdEquiv∙ = isoToEquiv ⋀lIdIso
+snd ⋀lIdEquiv∙ = refl
+
+⋀lId-sq : (f : A →∙ B) →
+      (≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ (idfun∙ Bool*∙ ⋀→∙ f))
+    ≡ (f ∘∙ ≃∙map ⋀lIdEquiv∙)
+⋀lId-sq {ℓ} {A = A} {B = B} f =
+  ΣPathP ((funExt
+    (⋀-fun≡ _ _ (sym (snd f)) (λ x → h (fst x) (snd x)) hₗ hᵣ))
+  , (sym (rUnit refl) ◁ (λ i j → snd f (~ i ∨ j))
+    ▷ lUnit (snd f)))
+  where
+  h : (x : Lift Bool) (a : fst A)
+    → Bool⋀→ (inr (x , fst f a)) ≡ fst f (Bool⋀→ (inr (x , a)))
+  h (lift false) a = refl
+  h (lift true) a = sym (snd f)
+
+  hₗ : (x : Lift Bool)
+    → PathP (λ i → Bool⋀→ ((idfun∙ Bool*∙ ⋀→ f) (push (inl x) i))
+                   ≡ fst f (Bool⋀→ (push (inl x) i)))
+             (sym (snd f)) (h x (pt A))
+  hₗ (lift false) =
+    flipSquare ((cong-∙ (Bool⋀→ {ℓ})
+                  (push (inl false*))
+                  (λ i → inr (lift false , snd f (~ i)))
+              ∙ sym (lUnit (sym (snd f))))
+             ◁ λ i j → snd f (~ i ∧ ~ j))
+  hₗ (lift true) =
+    flipSquare
+       ((cong-∙ (Bool⋀→ {ℓ})
+         (push (inl true*)) (λ i → inr (lift true , snd f (~ i)))
+       ∙ sym (rUnit refl))
+      ◁ λ i _ → snd f (~ i))
+
+  hᵣ : (x : fst A)
+    → PathP (λ i → Bool⋀→ {ℓ} ((idfun∙ Bool*∙ ⋀→ f) (push (inr x) i))
+                   ≡ fst f (snd A))
+             (sym (snd f)) (h true* x)
+  hᵣ x = flipSquare ((cong-∙ (Bool⋀→ {ℓ})
+                      (push (inr (fst f x)))
+                      (λ i → inr (true* , fst f x))
+                    ∙ sym (rUnit refl))
+      ◁ λ i _ → snd f (~ i))
+
+⋀lId-assoc : ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→∙ idfun∙ B)
+             ∘∙ ≃∙map SmashAssocEquiv∙)
+            ≡ ≃∙map ⋀lIdEquiv∙
+⋀lId-assoc {ℓ} {A = A} {B = B} =
+  ΣPathP (funExt
+          (⋀-fun≡'.main _ _
+            (λ xy → mainᵣ (fst xy) (snd xy))
+            (λ x → sym (rUnit refl) ◁ mainᵣ-pt-coh x)
+            (⋀→∙Homogeneous≡ (isHomogeneousPath _ _) mainᵣ-coh))
+        , (sym (rUnit refl)
+          ◁ flipSquare (sym (rUnit refl))))
+  where
+  l₁ : (x : Lift Bool) → inl tt ≡ Bool⋀→ (inr (x , inl tt))
+  l₁ (lift true) = refl
+  l₁ (lift false) = refl
+
+  l₂ : (x : Lift Bool) (y : fst A × fst B)
+    → inr (Bool⋀→ (inr (x , fst y)) , snd y)
+    ≡ Bool⋀→ (inr (x , inr y))
+  l₂ (lift true) y = sym (push (inr (snd y)))
+  l₂ (lift false) y = refl
+
+  l₁≡l₂-left : (x : Lift Bool) (y : fst A) →
+    PathP (λ i → l₁ x i ≡ l₂ x (y , pt B) i)
+          (push (inl (Bool⋀→ (inr (x , y)))))
+          λ i → Bool⋀→ {ℓ} {A = A ⋀∙ B} (inr (x , push (inl y) i))
+  l₁≡l₂-left (lift true) y = (λ i → push (push tt i))
+                   ◁ λ i j → push (inr (pt B)) (~ i ∧ j)
+  l₁≡l₂-left (lift false) y = refl
+
+  l₁≡l₂-right : (x : Lift Bool) (y : fst B)
+    → PathP (λ i → l₁ x i ≡ l₂ x ((pt A) , y) i)
+            (push (inr y) ∙ (λ i → inr (Bool⋀→ {A = A} (push (inl x) i) , y)))
+            (λ i → Bool⋀→ {A = A ⋀∙ B} (inr (x , push (inr y) i)))
+  l₁≡l₂-right (lift false) y = sym (rUnit (push (inr y)))
+  l₁≡l₂-right (lift true) y = sym (rUnit (push (inr y)))
+                   ◁ λ i j → push (inr y) (j ∧ ~ i)
+
+  mainᵣ : (x : Lift Bool) (y : A ⋀ B)
+    → (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B)
+        (SmashAssocIso .Iso.fun (inr (x , y)))
+     ≡ Bool⋀→ {ℓ} (inr (x , y))
+  mainᵣ x = ⋀-fun≡ _ _ (l₁ x) (l₂ x)
+    (λ y → flipSquare (sym (rUnit (push (inl (Bool⋀→ (inr (x , y))))))
+          ◁ l₁≡l₂-left x y))
+    λ y → flipSquare (
+      (cong (cong (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B))
+            (cong-∙∙ ⋀comm→
+              (push (inl y)) (λ i → inr (y , push (inl x) i)) refl
+          ∙ sym (compPath≡compPath'
+                  (push (inr y)) (λ i → inr (push (inl x) i , y))))
+        ∙ cong-∙ (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B)
+            (push (inr y)) λ i → inr (push (inl x) i , y))
+        ◁ (cong₂ _∙_ (sym (rUnit (push (inr y))))
+                     refl
+                   ◁ l₁≡l₂-right x y))
+
+  mainᵣ-pt-coh : (x : Lift Bool)
+    → PathP (λ i → inl tt ≡ Bool⋀→ (push (inl x) i))
+             refl (mainᵣ x (inl tt))
+  mainᵣ-pt-coh (lift false) = refl
+  mainᵣ-pt-coh (lift true) = refl
+
+  module N = ⋀-fun≡'
+    (λ z → (≃∙map ⋀lIdEquiv∙ ⋀→ idfun∙ B) (SmashAssocIso .Iso.fun z))
+    (λ z → ⋀lIdIso .Iso.fun z)
+    (λ xy → mainᵣ (fst xy) (snd xy))
+  open N
+
+  lem : (x : fst A) (y : fst B)
+    → cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→ idfun∙ B)
+            ∘ SmashAssocIso .Iso.fun)
+             (push (inr (inr (x , y))))
+    ≡ push (inr y)
+  lem x y =
+      cong (cong (≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→ idfun∙ B))
+            (cong-∙∙ ⋀comm→
+              (push (inl y)) (λ i → inr (y , push (inr x) i)) refl
+           ∙ sym (compPath≡compPath'
+                  (push (inr y)) λ i → inr (push (inr x) i , y)))
+    ∙∙ cong-∙ (≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ⋀→ idfun∙ B)
+              (push (inr y))
+              (λ i → inr (push (inr x) i , y))
+    ∙∙ (sym (rUnit _)
+     ∙ sym (rUnit _))
+
+  mainᵣ-coh : (x : fst A) (y : fst B)
+    → Fₗ .fst (inr (x , y)) ≡ Fᵣ .fst (inr (x , y))
+  mainᵣ-coh x y =
+      (λ i → lem x y i ∙∙ sym (lem x y i1) ∙∙ refl)
+    ∙ sym (compPath≡compPath'
+           (push (inr y)) (sym (push (inr y))))
+    ∙ rCancel (push (inr y))
+    ∙ rUnit refl
+
+-- Triangle equality
+⋀triang : ∀ {ℓ} {A B : Pointed ℓ}
+  → (((≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ ⋀comm→∙) ⋀→∙ idfun∙ B)
+    ∘∙ ≃∙map SmashAssocEquiv∙)
+    ≡ idfun∙ A ⋀→∙ ≃∙map (⋀lIdEquiv∙ {ℓ} {A = B})
+⋀triang {ℓ = ℓ} {A = A} {B = B} =
+  ΣPathP ((funExt (⋀-fun≡'.main _ _
+    (λ x → mainᵣ (fst x) (snd x))
+    (λ x → p≡refl
+         ◁ flipSquare ((λ i j → push (inl x) (i ∧ j))
+         ▷ rUnit (push (inl x))))
+    (⋀→∙Homogeneous≡ (isHomogeneousPath _ _)
+      λ x y → Fₗ≡refl x y ∙ sym (Fᵣ≡refl x y))))
+    , (sym (rUnit refl) ◁ flipSquare p≡refl))
+  where
+  mainᵣ-hom : (x : fst A) (y : Bool* {ℓ}) (z : fst B)
+    → Path (A ⋀ B) (inr (Bool⋀→ (inr (y , x)) , z))
+                    (inr (x , Bool⋀→ (inr (y , z))))
+  mainᵣ-hom x (lift false) z = refl
+  mainᵣ-hom x (lift true) z = sym (push (inr z)) ∙ push (inl x)
+
+  mainᵣ : (x : fst A) (y : Bool*∙ {ℓ} ⋀ B) →
+    ((≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ ⋀comm→∙) ⋀→ (idfun∙ B))
+      (Iso.fun (SmashAssocIso {A = A} {B = Bool*∙ {ℓ}} {C = B}) (inr (x , y)))
+    ≡ inr (x , ⋀lIdIso .Iso.fun y)
+  mainᵣ x = ⋀-fun≡ _ _ (push (inl x))
+    (λ y → mainᵣ-hom x (fst y) (snd y))
+    (λ { (lift false) → flipSquare (sym (rUnit (push (inl x)))
+                       ◁ λ i j → push (inl x) (j ∨ i))
+       ; (lift true) → flipSquare ((sym (rUnit (push (inl (pt A))))
+                                   ∙ λ j i → push (push tt j) i)
+                     ◁ λ i j → compPath-filler'
+                                 (sym (push (inr (pt B)))) (push (inl x)) j i)})
+     λ b → flipSquare
+       ((cong (cong (((≃∙map (⋀lIdEquiv∙ {ℓ}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)))
+         (cong-∙∙ ⋀comm→ (push (inl b)) (λ i → inr (b , push (inl x) i)) refl
+         ∙ sym (compPath≡compPath'
+                 (push (inr b)) (λ i → inr (push (inl x) i , b))))
+       ∙ cong-∙ (((≃∙map (⋀lIdEquiv∙ {ℓ})  ∘∙ ⋀comm→∙) ⋀→ idfun∙ B))
+                (push (inr b)) (λ i → inr (push (inl x) i , b))
+       ∙ sym (rUnit _)
+       ∙ (λ i → (push (inr b) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , b))))
+       ∙ sym (rUnit (push (inr b))))
+       ◁ λ i j → compPath-filler' (sym (push (inr b))) (push (inl x)) j i)
+
+  lemₗ : cong (idfun∙ A ⋀→ ≃∙map (⋀lIdEquiv∙ {ℓ} {A = B}))
+             (push (inr (inl tt)))
+      ≡ (push (inl (snd A)))
+  lemₗ = sym (rUnit _) ∙ λ i → push (push tt (~ i))
+
+  module K = ⋀-fun≡' (λ z →
+          ((≃∙map ⋀lIdEquiv∙ ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
+          (SmashAssocIso .Iso.fun z))
+       (λ z → (idfun∙ A ⋀→ ≃∙map ⋀lIdEquiv∙) z)
+       (λ x₁ → mainᵣ (fst x₁) (snd x₁))
+  open K
+
+  p≡refl : p ≡ refl
+  p≡refl = cong (push (inl (snd A)) ∙_) (cong sym lemₗ)
+         ∙ rCancel (push (inl (pt A)))
+
+  Fₗ-false : (y : fst B)
+    → cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
+        (cong ⋀comm→ (push (inl y)
+                   ∙' (λ i → inr (y , push (inr (lift false)) i))))
+      ≡ push (inr y)
+  Fₗ-false y =
+      cong (cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B))
+         (cong (cong ⋀comm→)
+           (sym (compPath≡compPath'
+             (push (inl y)) (λ i → inr (y , push (inr (lift false)) i))))
+       ∙ cong-∙ ⋀comm→ (push (inl y))
+                        (λ i → inr (y , push (inr (lift false)) i)))
+    ∙∙ cong-∙ ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
+              (push (inr y)) (λ i → inr (push (inr (lift false)) i , y))
+    ∙∙ (sym (rUnit _)
+     ∙ (λ i → push (inr y) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , y)))
+     ∙ sym (rUnit _))
+
+  Fₗ-true : (y : fst B)
+    → cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
+        (cong (SmashAssocIso .Iso.fun) (push (inr (inr (lift true , y)))))
+      ≡ push (inr y)
+  Fₗ-true y =
+      cong (cong ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B))
+        (cong-∙∙ ⋀comm→ (push (inl y)) (λ i → inr (y , push (inr true*) i)) refl
+        ∙ sym (compPath≡compPath' (push (inr y))
+                                  λ i → inr (push (inr true*) i , y)))
+    ∙∙ cong-∙ ((≃∙map (⋀lIdEquiv∙ {ℓ} {A = A}) ∘∙ ⋀comm→∙) ⋀→ idfun∙ B)
+              (push (inr y))
+              (λ i → inr (push (inr true*) i , y))
+    ∙∙ ((sym (rUnit _)
+     ∙ (λ i → push (inr y) ∙ (λ j → inr (rUnit (λ _ → pt A) (~ i) j , y)))
+     ∙ sym (rUnit _)))
+
+  Fₗ≡refl : (x : Lift Bool) (y : fst B) → Fₗ .fst (inr (x , y)) ≡ refl
+  Fₗ≡refl (lift false) y =
+     (λ i → Fₗ-false y i ∙∙ refl ∙∙ sym (rUnit (push (inr y)) (~ i)))
+    ∙ ∙∙lCancel _
+  Fₗ≡refl (lift true) y =
+      (λ j → Fₗ-true y j
+          ∙∙ (sym (push (inr y)) ∙ push (push tt j))
+          ∙∙ sym (rUnit (push (inr (pt B))) (~ j)))
+    ∙ (λ j → (λ i → push (inr y) (i ∧ ~ j))
+           ∙∙ (λ i → push (inr y) (~ j ∧ ~ i))
+            ∙ push (inr (pt B))
+           ∙∙ sym (push (inr (pt B))))
+    ∙ cong (_∙ sym (push (inr (pt B)))) (sym (lUnit (push (inr (pt B)))))
+    ∙ rCancel _
+
+  Fᵣ≡refl : (x : Lift Bool) (y : fst B) → Fᵣ .fst (inr (x , y)) ≡ refl
+  Fᵣ≡refl x y =
+    cong (push (inl (snd A)) ∙_)
+      (sym (rUnit _) ∙ (λ i j → push (push tt (~ i)) (~ j)))
+    ∙ rCancel _
\ No newline at end of file diff --git a/Cubical.HITs.SmashProduct.SymmetricMonoidalCat.html b/Cubical.HITs.SmashProduct.SymmetricMonoidalCat.html new file mode 100644 index 0000000000..c2aeab3979 --- /dev/null +++ b/Cubical.HITs.SmashProduct.SymmetricMonoidalCat.html @@ -0,0 +1,98 @@ + +Cubical.HITs.SmashProduct.SymmetricMonoidalCat
{-# OPTIONS --safe #-}
+
+{-
+This file contians a proof that the smash product turns the universe
+of pointed types into a symmetric monoidal wild category. The pentagon
+and hexagon are proved in separate files due to the length of the
+proofs. The remaining identities and the main result are proved here.
+-}
+
+module Cubical.HITs.SmashProduct.SymmetricMonoidalCat where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Sigma using (ΣPathP)
+open import Cubical.Data.Bool
+open import Cubical.HITs.SmashProduct.Base
+open import Cubical.HITs.SmashProduct.Pentagon
+open import Cubical.HITs.SmashProduct.Hexagon
+open import Cubical.HITs.SmashProduct.SymmetricMonoidal
+
+open import Cubical.WildCat.Base
+open import Cubical.WildCat.Functor
+open import Cubical.WildCat.Product
+open import Cubical.WildCat.BraidedSymmetricMonoidal
+open import Cubical.WildCat.Instances.Pointed
+
+open WildCat
+open WildFunctor
+open isSymmetricWildCat
+open isMonoidalWildCat
+open WildNatIso
+open WildNatTrans
+open wildIsIso
+
+private
+  variable
+    ℓ ℓ' : Level
+
+-- ⋀ as a functor
+⋀F : ∀ {ℓ} → WildFunctor (PointedCat ℓ × PointedCat ℓ) (PointedCat ℓ)
+F-ob ⋀F (A , B) = A ⋀∙ B
+F-hom ⋀F (f , g) = f ⋀→∙ g
+F-id ⋀F = ⋀→∙-idfun
+F-seq ⋀F (f , g) (f' , g') = ⋀→∙-comp f f' g g'
+
+⋀lUnitNatIso : WildNatIso (PointedCat ℓ) (PointedCat ℓ)
+      (restrFunctorₗ ⋀F Bool*∙) (idWildFunctor (PointedCat ℓ))
+N-ob (trans ⋀lUnitNatIso) X = ≃∙map ⋀lIdEquiv∙
+N-hom (trans ⋀lUnitNatIso) f = ⋀lId-sq f
+inv' (isIs ⋀lUnitNatIso c) = ≃∙map (invEquiv∙ ⋀lIdEquiv∙)
+sect (isIs (⋀lUnitNatIso {ℓ = ℓ}) c) =
+  ≃∙→ret/sec∙ (⋀lIdEquiv∙ {ℓ = ℓ} {A = c}) .snd
+retr (isIs ⋀lUnitNatIso c) =
+  ≃∙→ret/sec∙ ⋀lIdEquiv∙ .fst
+
+makeIsIso-Pointed : ∀ {ℓ} {A B : Pointed ℓ} {f : A →∙ B}
+  → isEquiv (fst f) → wildIsIso {C = PointedCat ℓ} f
+inv' (makeIsIso-Pointed {f = f} eq) = ≃∙map (invEquiv∙ ((fst f , eq) , snd f))
+sect (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f)  .snd
+retr (makeIsIso-Pointed {f = f} eq) = ≃∙→ret/sec∙ ((fst f , eq) , snd f)  .fst
+
+restrₗᵣ : WildNatIso (PointedCat ℓ) (PointedCat ℓ)
+      (restrFunctorᵣ ⋀F Bool*∙) (restrFunctorₗ ⋀F Bool*∙)
+N-ob (trans restrₗᵣ) X = ⋀comm→∙
+N-hom (trans restrₗᵣ) f = ⋀comm-sq f (idfun∙ Bool*∙)
+isIs restrₗᵣ c = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso)
+
+-- main result
+⋀Symm : ∀ {ℓ} → isSymmetricWildCat (PointedCat ℓ)
+_⊗_ (isMonoidal ⋀Symm) = ⋀F
+𝟙 (isMonoidal ⋀Symm) = Bool*∙
+N-ob (trans (⊗assoc (isMonoidal ⋀Symm))) (A , B , C) = ≃∙map SmashAssocEquiv∙
+N-hom (trans (⊗assoc (isMonoidal ⋀Symm))) (f , g , h) = ⋀assoc-⋀→∙ f g h
+inv' (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) =
+  ≃∙map (invEquiv∙ SmashAssocEquiv∙)
+sect (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) =
+  ≃∙→ret/sec∙ SmashAssocEquiv∙ .snd
+retr (isIs (⊗assoc (isMonoidal ⋀Symm)) (A , B , C)) =
+  ≃∙→ret/sec∙ SmashAssocEquiv∙ .fst
+⊗lUnit (isMonoidal ⋀Symm) = ⋀lUnitNatIso
+⊗rUnit (isMonoidal ⋀Symm) = compWildNatIso _ _ _ restrₗᵣ ⋀lUnitNatIso
+triang (isMonoidal (⋀Symm {ℓ})) X Y = ⋀triang
+⊗pentagon (isMonoidal ⋀Symm) X Y Z W =
+  (∘∙-assoc assc₅∙ assc₄∙ assc₃∙) ∙ pentagon∙
+N-ob (trans (Braid ⋀Symm)) X = ⋀comm→∙
+N-hom (trans (Braid ⋀Symm)) (f , g) = ⋀comm-sq f g
+isIs (Braid ⋀Symm) _ = makeIsIso-Pointed (isoToIsEquiv ⋀CommIso)
+isSymmetricWildCat.hexagon ⋀Symm a b c = hexagon∙
+symBraiding ⋀Symm X Y =
+  ΣPathP ((funExt (Iso.rightInv ⋀CommIso)) , (sym (rUnit refl)))
+
\ No newline at end of file diff --git a/Cubical.Papers.SmashProducts.html b/Cubical.Papers.SmashProducts.html index 4f920d5493..57dea68401 100644 --- a/Cubical.Papers.SmashProducts.html +++ b/Cubical.Papers.SmashProducts.html @@ -15,108 +15,110 @@ {-# OPTIONS --safe #-} module Cubical.Papers.SmashProducts where -- Section 2 -import Cubical.Categories.Category.Precategory as WCat -import Cubical.HITs.SmashProduct.Base as Smash +import Cubical.WildCat.Base as WCat1 +import Cubical.WildCat.Instances.Pointed as WCat2 +import Cubical.WildCat.BraidedSymmetricMonoidal as WCat3 +import Cubical.HITs.SmashProduct.Base as Smash --- Section 3 -import Cubical.Foundations.Pointed.Homogeneous as Hom +-- Section 3 +import Cubical.Foundations.Pointed.Homogeneous as Hom --- Section 5 -import Cubical.HITs.SmashProduct.SymmetricMonoidal as SM +-- Section 5 +import Cubical.HITs.SmashProduct.SymmetricMonoidalCat as SM --- Section 6 -import Cubical.HITs.SmashProduct.Induction as SmashInduction +-- Section 6 +import Cubical.HITs.SmashProduct.Induction as SmashInduction ----- 2 Background ---- ---- 2.1 Symmetric monoidal wild categories +---- 2 Background ---- +--- 2.1 Symmetric monoidal wild categories --- Definition 1 (Wild categories - note: currently called precategories in the library) -open WCat using (Precategory) +-- Definition 1 (Wild categories) +open WCat1 using (WildCat) --- Proposition 2 (Pointed types form a wild cat) -open WCat using (PointedCat) +-- Proposition 2 (Pointed types form a wild cat) +open WCat2 using (PointedCat) --- Definition 3 (Monoidal wild categories) -open WCat using (isMonoidalPrecategory) +-- Definition 3 (Monoidal wild categories) +open WCat3 using (isMonoidalWildCat) --- Definition 4 (Symmetric Monoidal wild categories) -open WCat using (SymmetricMonoidalPrecat) +-- Definition 4 (Symmetric Monoidal wild categories) +open WCat3 using (SymmetricMonoidalPrecat) ---- 2.2 Smash Products --- Definition 5 (Smash products -- note: defined as a coproduct in the --- library. E.g. the ⟨ x , y ⟩ constructor here is simply --- inr(x,y). Also note that pushₗ and pushᵣ are inverted with this --- definition.) -open Smash using (_⋀_) +--- 2.2 Smash Products +-- Definition 5 (Smash products -- note: defined as a coproduct in the +-- library. E.g. the ⟨ x , y ⟩ constructor here is simply +-- inr(x,y). Also note that pushₗ and pushᵣ are inverted with this +-- definition.) +open Smash using (_⋀_) --- Definition 6 (Functorial action of ⋀) -open Smash using (_⋀→_) --- Proposition 7 (Commutativity of ⋀) --- Postponed -- stated as part of Theorem 21 +-- Definition 6 (Functorial action of ⋀) +open Smash using (_⋀→_) +-- Proposition 7 (Commutativity of ⋀) +-- Postponed -- stated as part of Theorem 21 ----- 3 Associativity ---- --- Definition 8 (Double smash product) -open Smash using (⋀×2) +---- 3 Associativity ---- +-- Definition 8 (Double smash product) +open Smash using (⋀×2) --- Equivalence between smash product and double smash -open Smash using (Iso-⋀-⋀×2) +-- Equivalence between smash product and double smash +open Smash using (Iso-⋀-⋀×2) --- Proposition 9 (Associativity of ⋀) --- Postponed -- stated as part of Theorem 21 +-- Proposition 9 (Associativity of ⋀) +-- Postponed -- stated as part of Theorem 21 ----- 4 The Heuristic ---- --- Lemma 10 (first induction principle for smash products) -open Smash using (⋀-fun≡) +---- 4 The Heuristic ---- +-- Lemma 10 (first induction principle for smash products) +open Smash using (⋀-fun≡) --- Definition 10 -open Smash using (⋀-fun≡) +-- Definition 10 +open Smash using (⋀-fun≡) --- Definition 11 (version using ≡ instead of ≃⋆ is used here) -open Hom using (isHomogeneous) +-- Definition 11 (version using ≡ instead of ≃⋆ is used here) +open Hom using (isHomogeneous) --- Lemma 12 (Evan's trick) -open Hom using (→∙Homogeneous≡) +-- Lemma 12 (Evan's trick) +open Hom using (→∙Homogeneous≡) --- Lemma 13 (Evan's trick for smash products) -open Smash using (⋀→∙Homogeneous≡) +-- Lemma 13 (Evan's trick for smash products) +open Smash using (⋀→∙Homogeneous≡) --- Lemma 14 (Evan's trick smash products, v2) -open Smash using (⋀→Homogeneous≡) +-- Lemma 14 (Evan's trick smash products, v2) +open Smash using (⋀→Homogeneous≡) --- Definition 15 -open Smash.⋀-fun≡' renaming (Fₗ to L ; Fᵣ to R) +-- Definition 15 +open Smash.⋀-fun≡' renaming (Fₗ to L ; Fᵣ to R) --- Lemma 16 -open Smash.⋀-fun≡' using (main) +-- Lemma 16 +open Smash.⋀-fun≡' using (main) --- Lemmas 17/18 --- Omitted (used implicitly in formalisation) +-- Lemmas 17/18 +-- Omitted (used implicitly in formalisation) ----- 5 The symmetric monoidal structure ---- --- Proposition 19/20 (Hexagon and pentagon) --- Postponed - stated as part of Theorem 21 +---- 5 The symmetric monoidal structure ---- +-- Proposition 19/20 (Hexagon and pentagon) +-- Postponed - stated as part of Theorem 21 --- Theorem 21 (Symmetric monoidal structure) -open SM using (⋀Symm) +-- Theorem 21 (Symmetric monoidal structure) +open SM using (⋀Symm) ---- 5.1 Back to Brunerie's thesis --- This section is only meant to be an informal discussion and has not --- been formalised, as stated in the paper. +--- 5.1 Back to Brunerie's thesis +-- This section is only meant to be an informal discussion and has not +-- been formalised, as stated in the paper. --- 6. A formal statement of the heuristic --- Definition 25 (FS) -open SmashInduction using (FS) +-- 6. A formal statement of the heuristic +-- Definition 25 (FS) +open SmashInduction using (FS) --- Definition 26 (⋀̃) -open SmashInduction using (⋀̃) +-- Definition 26 (⋀̃) +open SmashInduction using (⋀̃) --- Theorem 27 (⋀̃→⋀ induction with coherences) -open SmashInduction using (⋀̃→⋀-ind ; ⋀̃→⋀-ind-coh) +-- Theorem 27 (⋀̃→⋀ induction with coherences) +open SmashInduction using (⋀̃→⋀-ind ; ⋀̃→⋀-ind-coh) --- Corollary 28 (⋀̃→⋀ induction without) -open SmashInduction using (⋀̃→⋀-ind) +-- Corollary 28 (⋀̃→⋀ induction without) +open SmashInduction using (⋀̃→⋀-ind) --- Corollary 29 (⋀̃→⋀ induction for pointed maps) -open SmashInduction using (⋀̃→⋀-ind∙) +-- Corollary 29 (⋀̃→⋀ induction for pointed maps) +open SmashInduction using (⋀̃→⋀-ind∙) \ No newline at end of file diff --git a/Cubical.README.html b/Cubical.README.html index fc58341cd6..87201341fc 100644 --- a/Cubical.README.html +++ b/Cubical.README.html @@ -41,43 +41,46 @@ -- Properties and proofs about relations import Cubical.Relation.Everything --- Category theory -import Cubical.Categories.Everything +-- Wild category theory +import Cubical.WildCat.Everything --- Homotopy theory -import Cubical.Homotopy.Everything +-- Category theory +import Cubical.Categories.Everything --- Properties and kinds of Modalities -import Cubical.Modalities.Everything +-- Homotopy theory +import Cubical.Homotopy.Everything --- Various experiments using Cubical Agda -import Cubical.Experiments.Everything +-- Properties and kinds of Modalities +import Cubical.Modalities.Everything --- Other modules (TODO: add descriptions) -import Cubical.Induction.Everything -import Cubical.Structures.Everything +-- Various experiments using Cubical Agda +import Cubical.Experiments.Everything --- general definition of cohomology -import Cubical.Cohomology.Everything +-- Other modules (TODO: add descriptions) +import Cubical.Induction.Everything +import Cubical.Structures.Everything --- cohomology with constant Integer coefficients -import Cubical.ZCohomology.Everything +-- general definition of cohomology +import Cubical.Cohomology.Everything --- Algebra library (in development) -import Cubical.Algebra.Everything +-- cohomology with constant Integer coefficients +import Cubical.ZCohomology.Everything --- Various talks -import Cubical.Talks.Everything +-- Algebra library (in development) +import Cubical.Algebra.Everything --- Reflection -import Cubical.Reflection.Everything +-- Various talks +import Cubical.Talks.Everything --- Displayed univalent graphs -import Cubical.Displayed.Everything +-- Reflection +import Cubical.Reflection.Everything --- Various axioms and consequences -import Cubical.Axiom.Everything +-- Displayed univalent graphs +import Cubical.Displayed.Everything --- Automatic proving, solvers -import Cubical.Tactics.Everything +-- Various axioms and consequences +import Cubical.Axiom.Everything + +-- Automatic proving, solvers +import Cubical.Tactics.Everything \ No newline at end of file diff --git a/Cubical.WildCat.Base.html b/Cubical.WildCat.Base.html new file mode 100644 index 0000000000..eb6d2797ab --- /dev/null +++ b/Cubical.WildCat.Base.html @@ -0,0 +1,90 @@ + +Cubical.WildCat.Base
{-
+  wild categories, analogous to the formalization in Coq-HoTT
+
+  https://github.com/HoTT/Coq-HoTT/tree/master/theories/WildCat
+
+-}
+{-# OPTIONS --safe #-}
+module Cubical.WildCat.Base where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Sigma renaming (_×_ to _×'_)
+
+private
+  variable
+    ℓ ℓ' : Level
+
+record WildCat ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+  no-eta-equality
+  field
+    ob : Type ℓ
+    Hom[_,_] : ob → ob → Type ℓ'
+    id   : ∀ {x} → Hom[ x , x ]
+    _⋆_  : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
+    ⋆IdL : ∀ {x y} (f : Hom[ x , y ]) → id ⋆ f ≡ f
+    ⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ id ≡ f
+    ⋆Assoc : ∀ {u v w x} (f : Hom[ u , v ]) (g : Hom[ v , w ]) (h : Hom[ w , x ])
+      → (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h)
+
+  -- composition: alternative to diagramatic order
+  _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ]
+  g ∘ f = f ⋆ g
+
+open WildCat
+
+-- Helpful syntax/notation
+_[_,_] : (C : WildCat ℓ ℓ') → (x y : C .ob) → Type ℓ'
+_[_,_] = Hom[_,_]
+
+-- Needed to define this in order to be able to make the subsequence syntax declaration
+seq' : ∀ (C : WildCat ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
+seq' = _⋆_
+
+infixl 15 seq'
+syntax seq' C f g = f ⋆⟨ C ⟩ g
+
+-- composition
+comp' : ∀ (C : WildCat ℓ ℓ') {x y z} (g : C [ y , z ]) (f : C [ x , y ]) → C [ x , z ]
+comp' = _∘_
+
+infixr 16 comp'
+syntax comp' C g f = g ∘⟨ C ⟩ f
+
+-- Isomorphisms in wild categories (analogous to HoTT-terminology for maps between types)
+record WildCatIso (C : WildCat ℓ ℓ') (x y : C .ob) : Type ℓ' where
+  no-eta-equality
+  constructor wildiso
+  field
+    mor : C [ x , y ]
+    inv : C [ y , x ]
+    sec : inv ⋆⟨ C ⟩ mor ≡ C .id
+    ret : mor ⋆⟨ C ⟩ inv ≡ C .id
+
+idIso : {C : WildCat ℓ ℓ'} {x : C .ob} → WildCatIso C x x
+idIso {C = C} = wildiso (C .id ) (C .id) (C .⋆IdL (C .id)) (C .⋆IdL (C .id))
+
+pathToIso : {C : WildCat ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → WildCatIso C x y
+pathToIso {C = C} p = J (λ z _ → WildCatIso C _ z) idIso p
+
+-- Natural isomorphisms
+module _ {C : WildCat ℓ ℓ'}
+  {x y : C .ob} (f : Hom[_,_] C x y) where
+  record wildIsIso : Type (ℓ-max ℓ ℓ') where
+    no-eta-equality
+    field
+      inv' : Hom[_,_] C y x
+      sect : _⋆_ C inv' f ≡ id C {y}
+      retr : _⋆_ C f inv' ≡ id C {x}
+
+-- Opposite wild category
+_^op : WildCat ℓ ℓ' → WildCat ℓ ℓ'
+(C ^op) .ob = C .ob
+(C ^op) .Hom[_,_] x y = C .Hom[_,_] y x
+(C ^op) .id = C .id
+(C ^op) ._⋆_ f g = C ._⋆_ g f
+(C ^op) .⋆IdL = C .⋆IdR
+(C ^op) .⋆IdR = C .⋆IdL
+(C ^op) .⋆Assoc f g h = sym (C .⋆Assoc _ _ _)
+
\ No newline at end of file diff --git a/Cubical.WildCat.BraidedSymmetricMonoidal.html b/Cubical.WildCat.BraidedSymmetricMonoidal.html new file mode 100644 index 0000000000..ad7766991e --- /dev/null +++ b/Cubical.WildCat.BraidedSymmetricMonoidal.html @@ -0,0 +1,111 @@ + +Cubical.WildCat.BraidedSymmetricMonoidal
{-
+  Monoidal, braided and monoidal symmetric wild categories
+-}
+{-# OPTIONS --safe #-}
+module Cubical.WildCat.BraidedSymmetricMonoidal where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Sigma renaming (_×_ to _×'_)
+
+open import Cubical.WildCat.Base
+open import Cubical.WildCat.Product
+open import Cubical.WildCat.Functor
+
+private
+  variable
+    ℓ ℓ' : Level
+
+open WildCat
+
+open WildFunctor
+open WildNatTrans
+open WildNatIso
+open wildIsIso
+
+module _ (M : WildCat ℓ ℓ') where
+  record isMonoidalWildCat : Type (ℓ-max ℓ ℓ') where
+    field
+      _⊗_ : WildFunctor (M × M) M
+      𝟙 : ob M
+
+      ⊗assoc : WildNatIso (M × (M × M)) M (assocₗ _⊗_) (assocᵣ _⊗_)
+
+      ⊗lUnit : WildNatIso M M (restrFunctorₗ _⊗_ 𝟙) (idWildFunctor M)
+      ⊗rUnit : WildNatIso M M (restrFunctorᵣ _⊗_ 𝟙) (idWildFunctor M)
+
+    private
+      α = N-ob (trans ⊗assoc)
+      α⁻ : (c : ob M ×' ob M ×' ob M) → M [ _ , _ ]
+      α⁻ c = wildIsIso.inv' (isIs ⊗assoc c)
+      rId = N-ob (trans ⊗rUnit)
+      lId = N-ob (trans ⊗lUnit)
+
+    field
+      -- Note: associators are on the form x ⊗ (y ⊗ z) → (x ⊗ y) ⊗ z
+      triang : (a b : M .ob)
+        → α (a , 𝟙 , b) ⋆⟨ M ⟩ (F-hom _⊗_ ((rId a) , id M))
+          ≡ F-hom _⊗_ ((id M) , lId b)
+
+      ⊗pentagon : (a b c d : M .ob)
+        → (F-hom _⊗_ (id M , α (b , c , d)))
+           ⋆⟨ M ⟩ ((α (a , (_⊗_ .F-ob (b , c)) , d))
+           ⋆⟨ M ⟩ (F-hom _⊗_ (α (a , b , c) , id M)))
+        ≡  (α (a , b , (F-ob _⊗_ (c , d))))
+           ⋆⟨ M ⟩ (α((F-ob _⊗_ (a , b)) , c , d))
+
+  module _ (mon : isMonoidalWildCat) where
+    open isMonoidalWildCat mon
+    private
+      α = N-ob (trans ⊗assoc)
+      α⁻ : (c : ob M ×' ob M ×' ob M) → M [ _ , _ ]
+      α⁻ c = wildIsIso.inv' (isIs ⊗assoc c)
+
+    BraidingIsoType : Type _
+    BraidingIsoType = WildNatIso (M × M) M _⊗_ (comp-WildFunctor commFunctor _⊗_)
+
+    HexagonType₁ : (B : BraidingIsoType) → Type _
+    HexagonType₁ B = (x y z : M .ob) →
+      F-hom _⊗_ ((id M) , N-ob (trans B) (y , z))
+        ⋆⟨ M ⟩ α (x , z , y)
+        ⋆⟨ M ⟩ F-hom _⊗_ (N-ob (trans B) (x , z) , (id M))
+       ≡ α (x , y , z)
+        ⋆⟨ M ⟩ N-ob (trans B) ((F-ob _⊗_ (x , y)) , z)
+        ⋆⟨ M ⟩ α (z , x , y)
+
+    HexagonType₂ : (B : BraidingIsoType) → Type _
+    HexagonType₂ B = (x y z : M .ob) →
+      F-hom _⊗_ (N-ob (trans B) (x , y) , id M)
+        ⋆⟨ M ⟩ α⁻ (y , x , z)
+        ⋆⟨ M ⟩ F-hom _⊗_ ((id M) , N-ob (trans B) (x , z))
+       ≡ α⁻ (x , y , z)
+        ⋆⟨ M ⟩ N-ob (trans B) (x , F-ob _⊗_ (y , z))
+        ⋆⟨ M ⟩ α⁻ (y , z , x)
+
+    isSymmetricBraiding : (B : BraidingIsoType)
+      → Type _
+    isSymmetricBraiding B = (x y : M .ob) →
+      N-ob (trans B) (x , y) ⋆⟨ M ⟩ (N-ob (trans B) (y , x))
+      ≡ id M
+
+  record isBraidedWildCat : Type (ℓ-max ℓ ℓ') where
+    open isMonoidalWildCat
+    field
+      isMonoidal : isMonoidalWildCat
+      Braid : BraidingIsoType isMonoidal
+      hexagons : (x y z : M .ob)
+        → HexagonType₁ isMonoidal Braid
+        ×' HexagonType₂ isMonoidal Braid
+
+  record isSymmetricWildCat : Type (ℓ-max ℓ ℓ') where
+    field
+      isMonoidal : isMonoidalWildCat
+      Braid : BraidingIsoType isMonoidal
+      hexagon : HexagonType₁ isMonoidal Braid
+      symBraiding : isSymmetricBraiding isMonoidal Braid
+
+SymmetricMonoidalPrecat : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
+SymmetricMonoidalPrecat ℓ ℓ' =
+  Σ[ C ∈ WildCat ℓ ℓ' ] isSymmetricWildCat C
+
\ No newline at end of file diff --git a/Cubical.WildCat.Everything.html b/Cubical.WildCat.Everything.html new file mode 100644 index 0000000000..9dad06fcd2 --- /dev/null +++ b/Cubical.WildCat.Everything.html @@ -0,0 +1,13 @@ + +Cubical.WildCat.Everything
{-# OPTIONS --safe #-}
+module Cubical.WildCat.Everything where
+
+import Cubical.WildCat.Base
+import Cubical.WildCat.BraidedSymmetricMonoidal
+import Cubical.WildCat.Functor
+import Cubical.WildCat.Instances.Categories
+import Cubical.WildCat.Instances.Path
+import Cubical.WildCat.Instances.Pointed
+import Cubical.WildCat.Instances.Types
+import Cubical.WildCat.Product
+
\ No newline at end of file diff --git a/Cubical.WildCat.Functor.html b/Cubical.WildCat.Functor.html new file mode 100644 index 0000000000..f42f98eaa9 --- /dev/null +++ b/Cubical.WildCat.Functor.html @@ -0,0 +1,166 @@ + +Cubical.WildCat.Functor
{-# OPTIONS --safe #-}
+module Cubical.WildCat.Functor where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Sigma using (ΣPathP)
+
+open import Cubical.WildCat.Base
+open import Cubical.WildCat.Product
+
+open WildCat
+
+private
+  variable
+    ℓ ℓ' : Level
+    ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
+
+ -- Functors
+record WildFunctor (C : WildCat ℓC ℓC') (D : WildCat ℓD ℓD') :
+         Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
+  no-eta-equality
+
+  field
+    F-ob  : C .ob → D .ob
+    F-hom : {x y : C .ob} → C [ x , y ] → D [ F-ob x , F-ob y ]
+    F-id  : {x : C .ob} → F-hom {y = x} (id C) ≡ id D
+    F-seq : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ])
+          → F-hom (f ⋆⟨ C ⟩ g) ≡ (F-hom f) ⋆⟨ D ⟩ (F-hom g)
+
+-- Natural transformation
+record WildNatTrans (C : WildCat ℓC ℓC') (D : WildCat ℓD ℓD')
+         (F G : WildFunctor C D) :
+         Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
+  no-eta-equality
+
+  open WildFunctor
+
+  field
+    N-ob : (x : C .ob) → D [ F .F-ob x , G .F-ob x ]
+    N-hom : {x y : C .ob} (f : C [ x , y ])
+      → (F .F-hom f) ⋆⟨ D ⟩ (N-ob y) ≡ (N-ob x) ⋆⟨ D ⟩ (G .F-hom f)
+
+-- Natural isomorphisms
+record WildNatIso (C : WildCat ℓC ℓC') (D : WildCat ℓD ℓD')
+         (F G : WildFunctor C D) :
+         Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
+  open WildNatTrans
+
+  field
+    trans : WildNatTrans C D F G
+    isIs : (c : C .ob) → wildIsIso {C = D} (trans .N-ob c)
+
+open WildFunctor
+open WildNatTrans
+open WildNatIso
+open wildIsIso
+
+module _
+  {C : WildCat ℓC ℓC'} {D : WildCat ℓD ℓD'}
+  (F G H : WildFunctor C D) where
+
+  compWildNatTrans : WildNatTrans _ _ F G → WildNatTrans _ _ G H → WildNatTrans _ _ F H
+  N-ob (compWildNatTrans η γ) c = N-ob η c ⋆⟨ D ⟩ N-ob γ c
+  N-hom (compWildNatTrans η γ) {x = x} {y = y} f =
+    sym (⋆Assoc D _ _ _) ∙ cong (λ w → w ⋆⟨ D ⟩ (N-ob γ y)) (N-hom η f)
+    ∙ ⋆Assoc D _ _ _
+    ∙ cong  (D ⋆ N-ob η x) (N-hom γ f)
+    ∙ sym (⋆Assoc D _ _ _)
+
+  compWildNatIso : WildNatIso _ _ F G → WildNatIso _ _ G H → WildNatIso _ _ F H
+  trans (compWildNatIso isη isγ) = compWildNatTrans (trans isη) (trans isγ)
+  inv' (isIs (compWildNatIso isη isγ) c) = inv' (isIs isγ c) ⋆⟨ D ⟩ (inv' (isIs isη c))
+  sect (isIs (compWildNatIso isη isγ) c) =
+    ⋆Assoc D _ _ _
+    ∙ cong (D ⋆ inv' (isIs isγ c))
+       (sym (⋆Assoc D _ _ _)
+       ∙ cong (λ w → w ⋆⟨ D ⟩ (N-ob (trans isγ) c)) (sect (isIs isη c))
+       ∙ ⋆IdL D _)
+    ∙ sect (isIs isγ c)
+  retr (isIs (compWildNatIso isη isγ) c) =
+    ⋆Assoc D _ _ _
+    ∙ cong (D ⋆ N-ob (trans isη) c)
+        (sym (⋆Assoc D _ _ _)
+        ∙ cong (λ w → w ⋆⟨ D ⟩ (inv' (isIs isη c))) (retr (isIs isγ c))
+        ∙ ⋆IdL D _)
+    ∙ retr (isIs isη c)
+
+module _
+  {C : WildCat ℓC ℓC'} {D : WildCat ℓD ℓD'} {E : WildCat ℓE ℓE'}
+ where
+ comp-WildFunctor : (F : WildFunctor C D) (G : WildFunctor D E)
+   → WildFunctor C E
+ F-ob (comp-WildFunctor F G) c = F-ob G (F-ob F c)
+ F-hom (comp-WildFunctor F G) f = F-hom G (F-hom F f)
+ F-id (comp-WildFunctor F G) = cong (F-hom G) (F-id F) ∙ F-id G
+ F-seq (comp-WildFunctor F G) f g = cong (F-hom G) (F-seq F f g) ∙ F-seq G _ _
+
+
+module _ {C : WildCat ℓC ℓC'}
+  (F : WildFunctor (C × C) C) where
+  assocₗ : WildFunctor (C × (C × C)) C
+  F-ob assocₗ (x , y , z) = F-ob F (x , F-ob F (y , z))
+  F-hom assocₗ {x} {y} (f , g) = F-hom F (f , F-hom F g)
+  F-id assocₗ =
+    cong (λ y → F-hom F (id C , y)) (F-id {C = C × C} F)
+      ∙ F-id F
+  F-seq assocₗ f g =
+    cong (F-hom F)
+         (cong (fst (f ⋆⟨ C × (C × C) ⟩ g) ,_)
+           (F-seq F (snd f) (snd g)))
+       ∙ F-seq F _ _
+
+  assocᵣ : WildFunctor (C × (C × C)) C
+  F-ob assocᵣ (x , y , z) = F-ob F (F-ob F (x , y) , z)
+  F-hom assocᵣ (f , g) = F-hom F (F-hom F (f , (fst g)) , snd g)
+  F-id assocᵣ = cong (F-hom F) (cong (_, id C) (F-id F))
+              ∙ F-id F
+  F-seq assocᵣ (f , f' , f'') (g , g' , g'') =
+    cong (F-hom F) (cong (_, _⋆_ C f'' g'')
+      (F-seq F (f , f') (g , g')))
+    ∙ F-seq F _ _
+
+-- Left and right restrictions of functors
+module _
+      {C : WildCat ℓC ℓC'}
+      {D : WildCat ℓD ℓD'}
+      {E : WildCat ℓE ℓE'}
+      where
+ restrFunctorₗ : (F : WildFunctor (C × D) E) (c : C . ob)
+   → WildFunctor D E
+ F-ob (restrFunctorₗ F c) d = F-ob F (c , d)
+ F-hom (restrFunctorₗ F c) f = F-hom F (id C , f)
+ F-id (restrFunctorₗ F c) = F-id F
+ F-seq (restrFunctorₗ F c) f g =
+     cong (F-hom F) (ΣPathP (sym (⋆IdR C _) , refl))
+   ∙ F-seq F (id C , f) (id C , g)
+
+ restrFunctorᵣ : (F : WildFunctor (C × D) E) (d : D . ob)
+   → WildFunctor C E
+ F-ob (restrFunctorᵣ F d) c = F-ob F (c , d)
+ F-hom (restrFunctorᵣ F d) f = F-hom F (f , (id D))
+ F-id (restrFunctorᵣ F d) = F-id F
+ F-seq (restrFunctorᵣ F d) f g =
+     cong (F-hom F) (ΣPathP (refl , sym (⋆IdR D _)))
+   ∙ F-seq F (f , id D) (g , id D)
+
+-- Identity functor
+idWildFunctor : {ℓC ℓC' : Level}
+      (C : WildCat ℓC ℓC')
+   → WildFunctor C C
+WildFunctor.F-ob (idWildFunctor C) c = c
+WildFunctor.F-hom (idWildFunctor C) x = x
+WildFunctor.F-id (idWildFunctor C) = refl
+WildFunctor.F-seq (idWildFunctor C) _ _ = refl
+
+-- Commutator
+commFunctor : {ℓC ℓC' ℓD ℓD' : Level}
+      {C : WildCat ℓC ℓC'}
+      {D : WildCat ℓD ℓD'}
+   → WildFunctor (C × D) (D × C)
+WildFunctor.F-ob commFunctor (x , y) = y , x
+WildFunctor.F-hom commFunctor (f , g) = g , f
+WildFunctor.F-id commFunctor = refl
+WildFunctor.F-seq commFunctor _ _ = refl
+
\ No newline at end of file diff --git a/Cubical.WildCat.Instances.Categories.html b/Cubical.WildCat.Instances.Categories.html new file mode 100644 index 0000000000..38ee1cd08b --- /dev/null +++ b/Cubical.WildCat.Instances.Categories.html @@ -0,0 +1,28 @@ + +Cubical.WildCat.Instances.Categories
-- The wild category of (small) categories
+{-# OPTIONS --safe #-}
+
+module Cubical.WildCat.Instances.Categories where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Functor.Properties
+
+open import Cubical.WildCat.Base
+
+module _ (ℓ ℓ' : Level) where
+  open WildCat
+
+  CatWildCat : WildCat (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-max ℓ ℓ')
+  CatWildCat .ob = Category ℓ ℓ'
+  CatWildCat .Hom[_,_] = Functor
+  CatWildCat .id = 𝟙⟨ _ ⟩
+  CatWildCat ._⋆_ G H = H ∘F G
+  CatWildCat .⋆IdL _ = F-lUnit
+  CatWildCat .⋆IdR _ = F-rUnit
+  CatWildCat .⋆Assoc _ _ _ = F-assoc
+
+-- TODO: what is required for Functor C D to be a set?
+
\ No newline at end of file diff --git a/Cubical.WildCat.Instances.Path.html b/Cubical.WildCat.Instances.Path.html new file mode 100644 index 0000000000..600eb79d0e --- /dev/null +++ b/Cubical.WildCat.Instances.Path.html @@ -0,0 +1,24 @@ + +Cubical.WildCat.Instances.Path
{-# OPTIONS --safe #-}
+module Cubical.WildCat.Instances.Path where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.GroupoidLaws
+
+open import Cubical.WildCat.Base
+
+private
+  variable
+    ℓ : Level
+
+open WildCat
+
+PathCat : (A : Type ℓ) → WildCat ℓ ℓ
+ob (PathCat A) = A
+Hom[_,_] (PathCat A) x y = (x ≡ y)
+id (PathCat A) = refl
+_⋆_ (PathCat A) = _∙_
+⋆IdL (PathCat A) p = sym (lUnit p)
+⋆IdR (PathCat A) p = sym (rUnit p)
+⋆Assoc (PathCat A) p q r = sym (assoc p q r)
+
\ No newline at end of file diff --git a/Cubical.WildCat.Instances.Pointed.html b/Cubical.WildCat.Instances.Pointed.html new file mode 100644 index 0000000000..fe473a22ba --- /dev/null +++ b/Cubical.WildCat.Instances.Pointed.html @@ -0,0 +1,20 @@ + +Cubical.WildCat.Instances.Pointed
{-# OPTIONS --safe #-}
+module Cubical.WildCat.Instances.Pointed where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed hiding (⋆ ; id)
+
+open import Cubical.WildCat.Base
+
+open WildCat
+
+PointedCat : (ℓ : Level) → WildCat (ℓ-suc ℓ) ℓ
+ob (PointedCat ℓ) = Pointed ℓ
+Hom[_,_] (PointedCat ℓ) A B = A →∙ B
+WildCat.id (PointedCat ℓ) = idfun∙ _
+_⋆_ (PointedCat ℓ) f g = g ∘∙ f
+⋆IdL (PointedCat ℓ) = ∘∙-idˡ
+⋆IdR (PointedCat ℓ) = ∘∙-idʳ
+⋆Assoc (PointedCat ℓ) f g h = sym (∘∙-assoc h g f)
+
\ No newline at end of file diff --git a/Cubical.WildCat.Instances.Types.html b/Cubical.WildCat.Instances.Types.html new file mode 100644 index 0000000000..c16b090df8 --- /dev/null +++ b/Cubical.WildCat.Instances.Types.html @@ -0,0 +1,21 @@ + +Cubical.WildCat.Instances.Types
{-# OPTIONS --safe #-}
+module Cubical.WildCat.Instances.Types where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed hiding (⋆ ; id)
+open import Cubical.Foundations.Function using (idfun) renaming (_∘_ to _∘fun_)
+
+open import Cubical.WildCat.Base
+
+open WildCat
+
+TypeCat : (ℓ : Level) → WildCat (ℓ-suc ℓ) ℓ
+ob (TypeCat ℓ) = Type ℓ
+Hom[_,_] (TypeCat ℓ) A B = A → B
+WildCat.id (TypeCat ℓ) = idfun _
+_⋆_ (TypeCat ℓ) f g = g ∘fun f
+⋆IdL (TypeCat ℓ) = λ _ → refl
+⋆IdR (TypeCat ℓ) = λ _ → refl
+⋆Assoc (TypeCat ℓ) f g h = refl
+
\ No newline at end of file diff --git a/Cubical.WildCat.Product.html b/Cubical.WildCat.Product.html new file mode 100644 index 0000000000..01a94e95aa --- /dev/null +++ b/Cubical.WildCat.Product.html @@ -0,0 +1,28 @@ + +Cubical.WildCat.Product
{-# OPTIONS --safe #-}
+module Cubical.WildCat.Product where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Sigma renaming (_×_ to _×'_)
+
+open import Cubical.WildCat.Base
+
+private
+  variable
+    ℓ ℓ' : Level
+    ℓC ℓC' ℓD ℓD' : Level
+
+open WildCat
+
+_×_ :  (C : WildCat ℓC ℓC') (D : WildCat ℓD ℓD') → WildCat _ _
+ob (C × D) = ob C ×' ob D
+Hom[_,_] (C × D) (c , d) (c' , d') =
+  Hom[_,_] C c c' ×' Hom[_,_] D d d'
+id (C × D) = id C , id D
+_⋆_ (C × D) f g = _⋆_ C (fst f) (fst g) , _⋆_ D (snd f) (snd g)
+⋆IdL (C × D) (f , g) i = (⋆IdL C f i) , (⋆IdL D g i)
+⋆IdR (C × D) (f , g) i = (⋆IdR C f i) , (⋆IdR D g i)
+⋆Assoc (C × D) (f , g) (f' , g') (f'' , g'') i =
+  ⋆Assoc C f f' f'' i , ⋆Assoc D g g' g'' i
+
\ No newline at end of file