Iterated cartesian products of higher groups

module higher-group-theory.iterated-cartesian-products-higher-groups where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.0-connected-types
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-cartesian-product-types
open import foundation.identity-types
open import foundation.iterated-cartesian-product-types
open import foundation.mere-equality
open import foundation.propositions
open import foundation.sets
open import foundation.unit-type
open import foundation.universe-levels

open import higher-group-theory.cartesian-products-higher-groups
open import higher-group-theory.higher-groups

open import structured-types.pointed-types

open import synthetic-homotopy-theory.loop-spaces

open import univalent-combinatorics.standard-finite-types

Idea

The iterated Cartesian product of a family of ∞-Group over Fin n is defined recursively on Fin n.

Definition

iterated-product-∞-Group :
  {l : Level} (n : ) (G : Fin n  (∞-Group l))  ∞-Group l
iterated-product-∞-Group zero-ℕ G = trivial-∞-Group
iterated-product-∞-Group (succ-ℕ n) G =
  product-∞-Group
    ( G (inr star))
    ( iterated-product-∞-Group n (G  inl))

module _
  {l : Level} (n : ) (G : Fin n  ∞-Group l)
  where

  classifying-pointed-type-iterated-product-∞-Group :
    Pointed-Type l
  classifying-pointed-type-iterated-product-∞-Group =
    pr1 (iterated-product-∞-Group n G)

  classifying-type-iterated-product-∞-Group : UU l
  classifying-type-iterated-product-∞-Group =
    type-Pointed-Type
      classifying-pointed-type-iterated-product-∞-Group

  shape-iterated-product-∞-Group :
    classifying-type-iterated-product-∞-Group
  shape-iterated-product-∞-Group =
    point-Pointed-Type
      classifying-pointed-type-iterated-product-∞-Group

  is-0-connected-classifying-type-iterated-product-∞-Group :
    is-0-connected classifying-type-iterated-product-∞-Group
  is-0-connected-classifying-type-iterated-product-∞-Group =
    pr2 (iterated-product-∞-Group n G)

  mere-eq-classifying-type-iterated-product-∞-Group :
    (X Y : classifying-type-iterated-product-∞-Group) 
    mere-eq X Y
  mere-eq-classifying-type-iterated-product-∞-Group =
    mere-eq-is-0-connected
      is-0-connected-classifying-type-iterated-product-∞-Group

  elim-prop-classifying-type-iterated-product-∞-Group :
    {l2 : Level}
    (P : classifying-type-iterated-product-∞-Group  Prop l2) 
    type-Prop (P shape-iterated-product-∞-Group) 
    ((X : classifying-type-iterated-product-∞-Group) 
    type-Prop (P X))
  elim-prop-classifying-type-iterated-product-∞-Group =
    apply-dependent-universal-property-is-0-connected
      shape-iterated-product-∞-Group
      is-0-connected-classifying-type-iterated-product-∞-Group

  type-iterated-product-∞-Group : UU (l)
  type-iterated-product-∞-Group =
    type-Ω classifying-pointed-type-iterated-product-∞-Group

  unit-iterated-product-∞-Group :
    type-iterated-product-∞-Group
  unit-iterated-product-∞-Group =
    refl-Ω classifying-pointed-type-iterated-product-∞-Group

  mul-iterated-product-∞-Group :
    (x y : type-iterated-product-∞-Group) 
    type-iterated-product-∞-Group
  mul-iterated-product-∞-Group =
    mul-Ω classifying-pointed-type-iterated-product-∞-Group

  assoc-mul-iterated-product-∞-Group :
    (x y z : type-iterated-product-∞-Group) 
    Id (mul-iterated-product-∞-Group
          ( mul-iterated-product-∞-Group x y)
          ( z))
       (mul-iterated-product-∞-Group
          ( x)
          ( mul-iterated-product-∞-Group y z))
  assoc-mul-iterated-product-∞-Group =
    associative-mul-Ω
      classifying-pointed-type-iterated-product-∞-Group

  left-unit-law-mul-iterated-product-∞-Group :
    (x : type-iterated-product-∞-Group) 
    Id (mul-iterated-product-∞-Group
          unit-iterated-product-∞-Group
          x)
       x
  left-unit-law-mul-iterated-product-∞-Group =
    left-unit-law-mul-Ω
      classifying-pointed-type-iterated-product-∞-Group

  right-unit-law-mul-iterated-product-∞-Group :
    (y : type-iterated-product-∞-Group) 
    Id (mul-iterated-product-∞-Group
          y
          unit-iterated-product-∞-Group)
       y
  right-unit-law-mul-iterated-product-∞-Group =
    right-unit-law-mul-Ω
      classifying-pointed-type-iterated-product-∞-Group

  coherence-unit-laws-mul-iterated-product-∞-Group :
    Id ( left-unit-law-mul-iterated-product-∞-Group
           unit-iterated-product-∞-Group)
       ( right-unit-law-mul-iterated-product-∞-Group
           unit-iterated-product-∞-Group)
  coherence-unit-laws-mul-iterated-product-∞-Group = refl

  inv-iterated-product-∞-Group :
    type-iterated-product-∞-Group  type-iterated-product-∞-Group
  inv-iterated-product-∞-Group =
    inv-Ω classifying-pointed-type-iterated-product-∞-Group

  left-inverse-law-mul-iterated-product-∞-Group :
    (x : type-iterated-product-∞-Group) 
    Id (mul-iterated-product-∞-Group
          ( inv-iterated-product-∞-Group x)
          ( x))
       unit-iterated-product-∞-Group
  left-inverse-law-mul-iterated-product-∞-Group =
    left-inverse-law-mul-Ω
      classifying-pointed-type-iterated-product-∞-Group

  right-inverse-law-mul-iterated-product-∞-Group :
    (x : type-iterated-product-∞-Group) 
    Id (mul-iterated-product-∞-Group
          ( x)
          ( inv-iterated-product-∞-Group x))
       unit-iterated-product-∞-Group
  right-inverse-law-mul-iterated-product-∞-Group =
    right-inverse-law-mul-Ω
      classifying-pointed-type-iterated-product-∞-Group

Properties

The type-∞-Group of a iterated product of a ∞-Group is the iterated product of the type-∞-Group

equiv-type-∞-Group-iterated-product-∞-Group :
  {l : Level} (n : ) (G : Fin n  ∞-Group l) 
  ( type-iterated-product-∞-Group n G) 
  ( iterated-product-Fin-recursive n (type-∞-Group  G))
equiv-type-∞-Group-iterated-product-∞-Group zero-ℕ G =
  equiv-is-contr
    ( is-proof-irrelevant-is-prop
        ( is-set-is-contr is-contr-raise-unit raise-star raise-star) refl)
    is-contr-raise-unit
equiv-type-∞-Group-iterated-product-∞-Group (succ-ℕ n) G =
  ( ( equiv-prod
        ( id-equiv)
        ( equiv-type-∞-Group-iterated-product-∞-Group
            ( n)
            (G  inl))) ∘e
    ( ( equiv-type-∞-Group-product-∞-Group
          ( G (inr star))
          ( iterated-product-∞-Group n (G  inl)))))