Finite multiplication in magmas

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-05-10.
Last modified on 2023-06-10.

module structured-types.finite-multiplication-magmas where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.unit-type
open import foundation.universe-levels

open import structured-types.magmas

open import univalent-combinatorics.counting
open import univalent-combinatorics.standard-finite-types

Definition

fold-Fin-mul-Magma :
  {l : Level} (M : Magma l)  type-Magma M 
  (k : )  (Fin k  type-Magma M)  type-Magma M
fold-Fin-mul-Magma M m zero-ℕ f = m
fold-Fin-mul-Magma M m (succ-ℕ k) f =
  mul-Magma M (fold-Fin-mul-Magma M m k (f  inl)) (f (inr star))

fold-count-mul-Magma' :
  {l1 l2 : Level} (M : Magma l1)  type-Magma M 
  {A : UU l2} (k : )  (Fin k  A)  (A  type-Magma M)  type-Magma M
fold-count-mul-Magma' M m k e f = fold-Fin-mul-Magma M m k (f  map-equiv e)

fold-count-mul-Magma :
  {l1 l2 : Level} (M : Magma l1)  type-Magma M 
  {A : UU l2}  count A  (A  type-Magma M)  type-Magma M
fold-count-mul-Magma M m e f =
  fold-Fin-mul-Magma M m (number-of-elements-count e) (f  map-equiv-count e)

Recent changes