DefinitionsAddMon, addMonToLaxMonoidal, addMonToLaxMonoidalObj, addUnitIso, counitIso, counitIsoAux, instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj, laxMonoidalToAddMon, hom, mk', X, addMon, comp, equivLaxMonoidalFunctorPUnit, forget, homInhabited, id, instAddMonObjTensorObj, instCategory, instInhabited, instMonoidalForget, instSymmetricCategory, mkIso, mkIso', monMonoidal, monMonoidalStruct, trivial, uniqueHomFromTrivial, AddMonObj, add, instTensorAddUnit, ofIso, instTensorObj, termζ, termσ, zero, «termζ[_]», «termσ[_]», mapAddMon, mapMon, mapAddMon, mapMon, addMonObj, mapAddMon, mapMon, monObj, addMonObjObj, instBraidedMonMapAddMon, instBraidedMonMapMon, instLaxBraidedMonMapAddMon, instLaxBraidedMonMapMon, instLaxMonoidalMonMapAddMon, instLaxMonoidalMonMapMon, instMonoidalMonMapAddMon, instMonoidalMonMapMon, mapAddMon, mapAddMonCompIso, mapAddMonFunctor, mapAddMonIdIso, mapAddMonNatIso, mapAddMonNatTrans, mapMon, mapMonCompIso, mapMonFunctor, mapMonIdIso, mapMonNatIso, mapMonNatTrans, monObjObj, IsAddMonHom, IsCommAddMonObj, IsCommMonObj, IsMonHom, Mon, counitIso, counitIsoAux, instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj, laxMonoidalToMon, monToLaxMonoidal, monToLaxMonoidalObj, unitIso, hom, mk', X, comp, equivLaxMonoidalFunctorPUnit, forget, homInhabited, id, instCategory, instInhabited, instMonObjTensorObj, instMonoidalForget, instSymmetricCategory, mkIso, mkIso', mon, monMonoidal, monMonoidalStruct, trivial, uniqueHomFromTrivial, MonObj, instTensorUnit, mul, ofIso, one, instTensorObj, termη, termμ, «termη[_]», «termμ[_]» | 110 |
TheoremsaddMonToLaxMonoidalObj_map, addMonToLaxMonoidalObj_obj, addMonToLaxMonoidalObj_ε, addMonToLaxMonoidalObj_μ, addMonToLaxMonoidal_laxMonoidalToAddMon_obj_add, addMonToLaxMonoidal_laxMonoidalToAddMon_obj_zero, addMonToLaxMonoidal_map_hom_app, addMonToLaxMonoidal_obj, addUnitIso_hom_app_hom_app, addUnitIso_inv_app_hom_app, counitIsoAux_hom, counitIsoAux_inv, counitIso_hom_app_hom, counitIso_inv_app_hom, isAddMonHom_counitIsoAux, laxMonoidalToAddMon_map, laxMonoidalToAddMon_obj, ext, ext', ext'_iff, ext_iff, isAddMonHom_hom, add_def, associator_hom_hom, associator_neg_hom, braiding_hom_hom, braiding_neg_hom, comp_hom, comp_hom', comp_hom'_assoc, equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom, equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom, equivLaxMonoidalFunctorPUnit_functor_map_hom, equivLaxMonoidalFunctorPUnit_functor_obj_X, equivLaxMonoidalFunctorPUnit_functor_obj_addMon_add, equivLaxMonoidalFunctorPUnit_functor_obj_addMon_zero, equivLaxMonoidalFunctorPUnit_inverse_map_hom_app, equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε, equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ, equivLaxMonoidalFunctorPUnit_inverse_obj_map, equivLaxMonoidalFunctorPUnit_inverse_obj_obj, equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_app, equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_app, forget_faithful, forget_map, forget_obj, forget_δ, forget_ε, forget_η, forget_μ, hom_injective, id_hom, id_hom', instHasInitial, instIsAddMonHomHom, instIsIsoHom, instIsIsoHomOfMapForget, instReflectsIsomorphismsForget, leftUnitor_hom_hom, leftUnitor_neg_hom, mkIso'_hom_hom, mkIso'_inv_hom, mkIso_hom_hom, mkIso_inv_hom, monMonoidalStruct_tensorHom_hom, monMonoidalStruct_tensorObj_X, rightUnitor_hom_hom, rightUnitor_neg_hom, tensorAddUnit_X, tensorAddUnit_add, tensorAddUnit_zero, tensorObj_add, tensorObj_zero, tensor_add, tensor_zero, trivial_X, trivial_addMon_add, trivial_addMon_zero, uniqueHomFromTrivial_default_hom, whiskerLeft_hom, whiskerRight_hom, zero_def, AddMon_tensor_add_assoc, AddMon_tensor_add_zero, AddMon_tensor_zero_add, add_add_add_comm, add_add_add_comm', add_add_add_comm'_assoc, add_add_add_comm_assoc, add_assoc, add_assoc_assoc, add_assoc_flip, add_assoc_flip_assoc, add_associator, add_braiding, add_def, add_leftUnitor, add_rightUnitor, add_zero, add_zero_assoc, add_zero_hom, add_zero_hom_assoc, ext, ext_iff, instIsAddMonHomHomAssociator, instIsAddMonHomHomBraiding, instIsAddMonHomHomLeftUnitor, instIsAddMonHomHomRightUnitor, instIsAddMonHomId, instIsAddMonHomTensorHom, instIsAddMonHomWhiskerLeft, instIsAddMonHomWhiskerRight, ofIso_add, ofIso_zero, add_def, zero_def, zero_add, zero_add_assoc, zero_add_hom, zero_add_hom_assoc, zero_associator, zero_braiding, zero_def, zero_leftUnitor, zero_rightUnitor, mapAddMon_counit, mapAddMon_unit, mapMon_counit, mapMon_unit, mapAddMon_counitIso, mapAddMon_functor, mapAddMon_inverse, mapAddMon_unitIso, mapMon_counitIso, mapMon_functor, mapMon_inverse, mapMon_unitIso, mapAddMon, mapMon, mapAddMon, mapMon, addMonObj_add, addMonObj_zero, isAddMonHom_preimage, isMonHom_preimage, mapAddMon_preimage_hom, mapMon_preimage_hom, monObj_mul, monObj_one, comp_mapAddMon_add, comp_mapAddMon_zero, comp_mapMon_mul, comp_mapMon_one, essImage_mapAddMon, essImage_mapMon, id_mapAddMon_add, id_mapAddMon_zero, id_mapMon_mul, id_mapMon_one, instIsAddMonHomε, instIsAddMonHomμ, instIsMonHomε, instIsMonHomμ, instIsAddMonHom, instIsMonHom, mapAddMonCompIso_hom_app_hom, mapAddMonCompIso_inv_app_hom, mapAddMonFunctor_map_app_hom, mapAddMonFunctor_obj, mapAddMonIdIso_hom_app_hom, mapAddMonIdIso_inv_app_hom, mapAddMonNatIso_hom_app_hom, mapAddMonNatIso_inv_app_hom, mapAddMonNatTrans_app_hom, mapAddMon_map_hom, mapAddMon_obj_X, mapAddMon_obj_addMon_add, mapAddMon_obj_addMon_zero, mapMonCompIso_hom_app_hom, mapMonCompIso_inv_app_hom, mapMonFunctor_map_app_hom, mapMonFunctor_obj, mapMonIdIso_hom_app_hom, mapMonIdIso_inv_app_hom, mapMonNatIso_hom_app_hom, mapMonNatIso_inv_app_hom, mapMonNatTrans_app_hom, mapMon_map_hom, mapMon_obj_X, mapMon_obj_mon_mul, mapMon_obj_mon_one, ζ_def, ζ_def_assoc, η_def, η_def_assoc, μ_def, μ_def_assoc, σ_def, σ_def_assoc, add_hom, add_hom_assoc, zero_hom, zero_hom_assoc, add_comm, add_comm', add_comm'_assoc, instTensorAddUnit, instTensorUnit, mul_comm, mul_comm', mul_comm'_assoc, mul_comm_assoc, mul_hom, mul_hom_assoc, one_hom, one_hom_assoc, add_assoc_hom, add_assoc_hom_assoc, add_assoc_neg, add_assoc_neg_assoc, associator_hom_comp_tensorHom_tensorHom, associator_hom_comp_tensorHom_tensorHom_assoc, associator_hom_comp_tensorHom_tensorHom_comp, associator_hom_comp_tensorHom_tensorHom_comp_assoc, associator_inv_comp_tensorHom_tensorHom, associator_inv_comp_tensorHom_tensorHom_assoc, associator_inv_comp_tensorHom_tensorHom_comp, associator_inv_comp_tensorHom_tensorHom_comp_assoc, eq_add_zero, eq_mul_one, eq_one_mul, eq_zero_add, leftUnitor_inv_one_tensor_mul, leftUnitor_inv_one_tensor_mul_assoc, leftUnitor_neg_zero_tensor_add, leftUnitor_neg_zero_tensor_add_assoc, mul_assoc_hom, mul_assoc_hom_assoc, mul_assoc_inv, mul_assoc_inv_assoc, rightUnitor_inv_tensor_one_mul, rightUnitor_inv_tensor_one_mul_assoc, rightUnitor_neg_tensor_zero_add, rightUnitor_neg_tensor_zero_add_assoc, counitIsoAux_hom, counitIsoAux_inv, counitIso_hom_app_hom, counitIso_inv_app_hom, isMonHom_counitIsoAux, laxMonoidalToMon_map, laxMonoidalToMon_obj, monToLaxMonoidalObj_map, monToLaxMonoidalObj_obj, monToLaxMonoidalObj_ε, monToLaxMonoidalObj_μ, monToLaxMonoidal_laxMonoidalToMon_obj_mul, monToLaxMonoidal_laxMonoidalToMon_obj_one, monToLaxMonoidal_map_hom_app, monToLaxMonoidal_obj, unitIso_hom_app_hom_app, unitIso_inv_app_hom_app, ext, ext', ext'_iff, ext_iff, isMonHom_hom, associator_hom_hom, associator_inv_hom, braiding_hom_hom, braiding_inv_hom, comp_hom, comp_hom', comp_hom'_assoc, equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom, equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom, equivLaxMonoidalFunctorPUnit_functor_map_hom, equivLaxMonoidalFunctorPUnit_functor_obj_X, equivLaxMonoidalFunctorPUnit_functor_obj_mon_mul, equivLaxMonoidalFunctorPUnit_functor_obj_mon_one, equivLaxMonoidalFunctorPUnit_inverse_map_hom_app, equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε, equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ, equivLaxMonoidalFunctorPUnit_inverse_obj_map, equivLaxMonoidalFunctorPUnit_inverse_obj_obj, equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_app, equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_app, forget_faithful, forget_map, forget_obj, forget_δ, forget_ε, forget_η, forget_μ, hom_injective, id_hom, id_hom', instHasInitial, instIsIsoHom, instIsIsoHomOfMapForget, instIsMonHomHom, instReflectsIsomorphismsForget, leftUnitor_hom_hom, leftUnitor_inv_hom, mkIso'_hom_hom, mkIso'_inv_hom, mkIso_hom_hom, mkIso_inv_hom, monMonoidalStruct_tensorHom_hom, monMonoidalStruct_tensorObj_X, mul_def, one_def, rightUnitor_hom_hom, rightUnitor_inv_hom, tensorObj_mul, tensorObj_one, tensorUnit_X, tensorUnit_mul, tensorUnit_one, tensor_mul, tensor_one, trivial_X, trivial_mon_mul, trivial_mon_one, uniqueHomFromTrivial_default_hom, whiskerLeft_hom, whiskerRight_hom, Mon_tensor_mul_assoc, Mon_tensor_mul_one, Mon_tensor_one_mul, ext, ext_iff, instIsMonHomHomAssociator, instIsMonHomHomBraiding, instIsMonHomHomLeftUnitor, instIsMonHomHomRightUnitor, instIsMonHomId, instIsMonHomTensorHom, instIsMonHomWhiskerLeft, instIsMonHomWhiskerRight, mul_assoc, mul_assoc_assoc, mul_assoc_flip, mul_assoc_flip_assoc, mul_associator, mul_braiding, mul_def, mul_leftUnitor, mul_mul_mul_comm, mul_mul_mul_comm', mul_mul_mul_comm'_assoc, mul_mul_mul_comm_assoc, mul_one, mul_one_assoc, mul_one_hom, mul_one_hom_assoc, mul_rightUnitor, ofIso_mul, ofIso_one, one_associator, one_braiding, one_def, one_leftUnitor, one_mul, one_mul_assoc, one_mul_hom, one_mul_hom_assoc, one_rightUnitor, mul_def, one_def, instIsAddMonHomComp, instIsAddMonHomHomAsIso, instIsAddMonHomId, instIsAddMonHomNegOfHom, instIsCommAddMonObjTensorObj, instIsCommMonObjTensorObj, instIsMonHomComp, instIsMonHomHomAsIso, instIsMonHomId, instIsMonHomInvOfHom, isAddMonHom_ofIso, isMonHom_ofIso | 381 |