Equations

• Mon_Type_equivalence_Mon.Mon_monoid A = {mul := λ (x y : A.X), A.mul (x, y), mul_assoc := _, one := A.one punit.star, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul A.X), npow_zero' := _, npow_succ' := _}

Converting a monoid object in Type to a bundled monoid.

Equations

• Mon_Type_equivalence_Mon.functor = {obj := λ (A : Mon_ (Type u)), {α := A.X, str := Mon_Type_equivalence_Mon.Mon_monoid A}, map := λ (A B : Mon_ (Type u)) (f : A ⟶ B), {to_fun := f.hom, map_one' := _, map_mul' := _}, map_id' := Mon_Type_equivalence_Mon.functor._proof_3, map_comp' := Mon_Type_equivalence_Mon.functor._proof_4}

Converting a bundled monoid to a monoid object in Type.

Equations

• Mon_Type_equivalence_Mon.inverse = {obj := λ (A : Mon), {X := ↥A, one := λ (_x : 𝟙_ (Type u)), 1, mul := λ (p : ↥A ⊗ ↥A), p.fst * p.snd, one_mul' := _, mul_one' := _, mul_assoc' := _}, map := λ (A B : Mon) (f : A ⟶ B), {hom := ⇑f, one_hom' := _, mul_hom' := _}, map_id' := Mon_Type_equivalence_Mon.inverse._proof_12, map_comp' := Mon_Type_equivalence_Mon.inverse._proof_13}

The category of internal monoid objects in Type is equivalent to the category of "native" bundled monoids.

Equations

• Mon_Type_equivalence_Mon = {functor := Mon_Type_equivalence_Mon.functor, inverse := Mon_Type_equivalence_Mon.inverse, unit_iso := category_theory.nat_iso.of_components (λ (A : Mon_ (Type u)), {hom := {hom := 𝟙 ((𝟭 (Mon_ (Type u))).obj A).X, one_hom' := _, mul_hom' := _}, inv := {hom := 𝟙 ((Mon_Type_equivalence_Mon.functor ⋙ Mon_Type_equivalence_Mon.inverse).obj A).X, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) Mon_Type_equivalence_Mon._proof_7, counit_iso := category_theory.nat_iso.of_components (λ (A : Mon), {hom := {to_fun := id ↥((Mon_Type_equivalence_Mon.inverse ⋙ Mon_Type_equivalence_Mon.functor).obj A), map_one' := _, map_mul' := _}, inv := {to_fun := id ↥((𝟭 Mon).obj A), map_one' := _, map_mul' := _}, hom_inv_id' := _, inv_hom_id' := _}) Mon_Type_equivalence_Mon._proof_14, functor_unit_iso_comp' := Mon_Type_equivalence_Mon._proof_15}

The equivalence Mon_ (Type u) ≌ Mon.{u} is naturally compatible with the forgetful functors to Type u.

Equations

• Mon_Type_equivalence_Mon_forget = category_theory.nat_iso.of_components (λ (A : Mon_ (Type u)), category_theory.iso.refl ((Mon_Type_equivalence_Mon.functor ⋙ category_theory.forget Mon).obj A)) Mon_Type_equivalence_Mon_forget._proof_1

Equations

• Mon_Type_inhabited = {default := Mon_Type_equivalence_Mon.inverse.obj (Mon.of punit)}

Equations

• CommMon_Type_equivalence_CommMon.CommMon_comm_monoid A = {mul := monoid.mul (Mon_Type_equivalence_Mon.Mon_monoid A.to_Mon_), mul_assoc := _, one := monoid.one (Mon_Type_equivalence_Mon.Mon_monoid A.to_Mon_), one_mul := _, mul_one := _, npow := monoid.npow (Mon_Type_equivalence_Mon.Mon_monoid A.to_Mon_), npow_zero' := _, npow_succ' := _, mul_comm := _}

Converting a commutative monoid object in Type to a bundled commutative monoid.

Equations

• CommMon_Type_equivalence_CommMon.functor = {obj := λ (A : CommMon_ (Type u)), {α := A.to_Mon_.X, str := CommMon_Type_equivalence_CommMon.CommMon_comm_monoid A}, map := λ (A B : CommMon_ (Type u)) (f : A ⟶ B), Mon_Type_equivalence_Mon.functor.map f, map_id' := CommMon_Type_equivalence_CommMon.functor._proof_1, map_comp' := CommMon_Type_equivalence_CommMon.functor._proof_2}

Converting a bundled commutative monoid to a commutative monoid object in Type.

Equations

• CommMon_Type_equivalence_CommMon.inverse = {obj := λ (A : CommMon), {to_Mon_ := {X := (Mon_Type_equivalence_Mon.inverse.obj ((category_theory.forget₂ CommMon Mon).obj A)).X, one := (Mon_Type_equivalence_Mon.inverse.obj ((category_theory.forget₂ CommMon Mon).obj A)).one, mul := (Mon_Type_equivalence_Mon.inverse.obj ((category_theory.forget₂ CommMon Mon).obj A)).mul, one_mul' := _, mul_one' := _, mul_assoc' := _}, mul_comm' := _}, map := λ (A B : CommMon) (f : A ⟶ B), Mon_Type_equivalence_Mon.inverse.map f, map_id' := CommMon_Type_equivalence_CommMon.inverse._proof_5, map_comp' := CommMon_Type_equivalence_CommMon.inverse._proof_6}

The category of internal commutative monoid objects in Type is equivalent to the category of "native" bundled commutative monoids.

Equations

• CommMon_Type_equivalence_CommMon = {functor := CommMon_Type_equivalence_CommMon.functor, inverse := CommMon_Type_equivalence_CommMon.inverse, unit_iso := category_theory.nat_iso.of_components (λ (A : CommMon_ (Type u)), {hom := {hom := 𝟙 ((𝟭 (CommMon_ (Type u))).obj A).to_Mon_.X, one_hom' := _, mul_hom' := _}, inv := {hom := 𝟙 ((CommMon_Type_equivalence_CommMon.functor ⋙ CommMon_Type_equivalence_CommMon.inverse).obj A).to_Mon_.X, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) CommMon_Type_equivalence_CommMon._proof_7, counit_iso := category_theory.nat_iso.of_components (λ (A : CommMon), {hom := {to_fun := id ↥((CommMon_Type_equivalence_CommMon.inverse ⋙ CommMon_Type_equivalence_CommMon.functor).obj A), map_one' := _, map_mul' := _}, inv := {to_fun := id ↥((𝟭 CommMon).obj A), map_one' := _, map_mul' := _}, hom_inv_id' := _, inv_hom_id' := _}) CommMon_Type_equivalence_CommMon._proof_14, functor_unit_iso_comp' := CommMon_Type_equivalence_CommMon._proof_15}

The equivalences Mon_ (Type u) ≌ Mon.{u} and CommMon_ (Type u) ≌ CommMon.{u} are naturally compatible with the forgetful functors to Mon and Mon_ (Type u).

Equations

• CommMon_Type_equivalence_CommMon_forget = category_theory.nat_iso.of_components (λ (A : CommMon_ (Type u)), category_theory.iso.refl ((CommMon_Type_equivalence_CommMon.functor ⋙ category_theory.forget₂ CommMon Mon).obj A)) CommMon_Type_equivalence_CommMon_forget._proof_1

Equations

• CommMon_Type_inhabited = {default := CommMon_Type_equivalence_CommMon.inverse.obj (CommMon.of punit)}