+ AddCommGrp.coyonedaObjIsoForget
+ AddCommGrp.forget_corepresentable
+ AddGrp.coyonedaObjIsoForget
+ AddGrp.forget_corepresentable
+ CommGrp
+ CommGrp.coyonedaObjIsoForget
+ CommGrp.forget_corepresentable
+ CommGrp.forget_reflects_isos
+ CommGrp.forget₂CommMonAdj
+ Grp
+ Grp.coyonedaObjIsoForget
+ Grp.forget_corepresentable
+ Grp.forget_reflects_isos
+ Grp.forget₂MonAdj
+ GrpWithZero
+ MonoidHom.comp_id_commGrp
+ MonoidHom.comp_id_grp
+ MonoidHom.id_commGrp_comp
+ MonoidHom.id_grp_comp
+ MulEquiv.toCommGrpIso
+ MulEquiv.toGrpIso
+ MulEquiv.toSemigrpIso
+ SemiNormedGrp
+ SemiNormedGrp₁
+ Semigrp
+ Semigrp.forgetReflectsIsos
+ Semigrp.forget₂_full
+ forget_commGrp_preserves_epi
+ forget_commGrp_preserves_mono
+ forget_grp_preserves_epi
+ forget_grp_preserves_mono
+ forget₂_addCommGrp_additive
+ forget₂_addCommGrp_essSurj
+ hasForgetToAddCommGrp
+ instance (G : CommGrp) : CommGroup <| (forget CommGrp).obj G
+ instance (G : Grp) : Group G.α
+ instance (G H : CommGrp) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
+ instance (G H : Grp) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
+ instance (M : SemiNormedGrp) : SeminormedAddCommGroup M
+ instance (M : SemiNormedGrp₁) : SeminormedAddCommGroup M
+ instance (P Q : AddCommGrp) : AddCommGroup (P ⟶ Q)
+ instance (X : Grp) : Group X := X.str
+ instance (X : GrpWithZero) : GroupWithZero X
+ instance (X : Semigrp) : Semigroup X := X.str
+ instance (X Y : SemiNormedGrp₁) : Zero (X ⟶ Y)
+ instance : (forget AddCommGrp.{u}).IsRightAdjoint
+ instance : (forget Grp.{u}).IsRightAdjoint
+ instance : (forget₂ (ModuleCat.{v} R) AddCommGrp.{v}).ReflectsIsomorphisms
+ instance : (forget₂ CommGrp.{u} Grp.{u}).ReflectsIsomorphisms
+ instance : Abelian AddCommGrp.{u}
+ instance : Coe CommGrp.{u} CommMonCat.{u} where coe := (forget₂ CommGrp CommMonCat).obj
+ instance : Coe CommGrp.{u} Grp.{u} where coe := (forget₂ CommGrp Grp).obj
+ instance : Coe Grp.{u} MonCat.{u} where coe := (forget₂ Grp MonCat).obj
+ instance : CoeSort CommGrp Type*
+ instance : CoeSort Grp Type*
+ instance : CoeSort GrpWithZero Type*
+ instance : CoeSort SemiNormedGrp Type*
+ instance : CoeSort SemiNormedGrp₁ Type*
+ instance : CoeSort Semigrp Type*
+ instance : ConcreteCategory SemiNormedGrp := by
+ instance : ConcreteCategory.{u} SemiNormedGrp₁
+ instance : HasBinaryBiproducts AddCommGrp
+ instance : HasCokernels SemiNormedGrp.{u}
+ instance : HasCokernels SemiNormedGrp₁.{u}
+ instance : HasColimitsOfSize.{0, 0} (AddCommGrp.{u}) := hasColimitsOfSize.{u, 0, 0}
+ instance : HasColimitsOfSize.{u, u} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{v}
+ instance : HasColimitsOfSize.{u, v} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{u}
+ instance : HasColimitsOfSize.{v, u} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{u}
+ instance : HasColimitsOfSize.{v, v} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{u}
+ instance : HasFiniteBiproducts AddCommGrp
+ instance : HasForget₂ SemiNormedGrp₁ SemiNormedGrp
+ instance : HasZeroObject CommGrp
+ instance : HasZeroObject Grp
+ instance : Inhabited (Action AddCommGrp G)
+ instance : Inhabited CommGrp
+ instance : Inhabited Grp
+ instance : Inhabited GrpWithZero
+ instance : Inhabited SemiNormedGrp
+ instance : Inhabited SemiNormedGrp₁
+ instance : Inhabited Semigrp
+ instance : LargeCategory.{u} GrpWithZero
+ instance : LargeCategory.{u} SemiNormedGrp₁
+ instance : Limits.HasEqualizers.{u, u + 1} SemiNormedGrp
+ instance : Limits.HasZeroMorphisms.{u, u + 1} SemiNormedGrp
+ instance : Limits.HasZeroMorphisms.{u, u + 1} SemiNormedGrp₁
+ instance : Preadditive AddCommGrp
+ instance : Preadditive SemiNormedGrp.{u}
+ instance : PreservesColimit F (forget₂ _ AddCommGrp)
+ instance : Small.{u} (Functor.sections ((F ⋙ forget₂ Grp MonCat) ⋙ forget MonCat))
+ instance _root_.AddCommGrp.forgetPreservesLimits :
+ instance {M N : GrpWithZero} : FunLike (M ⟶ N) M N
+ instance {M N : SemiNormedGrp} : Zero (M ⟶ N)
+ instance {V W : SemiNormedGrp.{u}} : NNNorm (V ⟶ W)
+ instance {V W : SemiNormedGrp.{u}} : Norm (V ⟶ W)
+ instance {V W : SemiNormedGrp.{u}} : Sub (V ⟶ W)
+ instance {X Y : CommGrp} : CoeFun (X ⟶ Y) fun _ => X → Y
+ instance {X Y : Grp} : CoeFun (X ⟶ Y) fun _ => X → Y
+ mulEquivIsoSemigrpIso
+ semigrpIsoToMulEquiv
+ toAddCommGrp
+ toAddGrp
+ toCommGrp
+ toGrp
+ wellPowered_addCommGrp
- AddCommGroupCat.coyonedaObjIsoForget
- AddCommGroupCat.forget_corepresentable
- AddGroupCat.coyonedaObjIsoForget
- AddGroupCat.forget_corepresentable
- CommGroupCat
- CommGroupCat.coyonedaObjIsoForget
- CommGroupCat.forget_corepresentable
- CommGroupCat.forget_reflects_isos
- CommGroupCat.forget₂CommMonAdj
- GroupCat
- GroupCat.coyonedaObjIsoForget
- GroupCat.forget_corepresentable
- GroupCat.forget_reflects_isos
- GroupCat.forget₂MonAdj
- GroupWithZeroCat
- MonoidHom.comp_id_commGroupCat
- MonoidHom.comp_id_groupCat
- MonoidHom.id_commGroupCat_comp
- MonoidHom.id_groupCat_comp
- MulEquiv.toCommGroupCatIso
- MulEquiv.toGroupCatIso
- MulEquiv.toSemigroupCatIso
- SemiNormedGroupCat
- SemiNormedGroupCat₁
- SemigroupCat
- SemigroupCat.forgetReflectsIsos
- SemigroupCat.forget₂_full
- forget_commGroupCat_preserves_epi
- forget_commGroupCat_preserves_mono
- forget_groupCat_preserves_epi
- forget_groupCat_preserves_mono
- forget₂_addCommGroupCat_additive
- forget₂_addCommGroupCat_essSurj
- hasForgetToAddCommGroupCat
- instance (G : CommGroupCat) : CommGroup <| (forget CommGroupCat).obj G
- instance (G : GroupCat) : Group G.α
- instance (G H : CommGroupCat) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
- instance (G H : GroupCat) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
- instance (M : SemiNormedGroupCat) : SeminormedAddCommGroup M
- instance (M : SemiNormedGroupCat₁) : SeminormedAddCommGroup M
- instance (P Q : AddCommGroupCat) : AddCommGroup (P ⟶ Q)
- instance (X : GroupCat) : Group X := X.str
- instance (X : GroupWithZeroCat) : GroupWithZero X
- instance (X : SemigroupCat) : Semigroup X := X.str
- instance (X Y : SemiNormedGroupCat₁) : Zero (X ⟶ Y)
- instance : (forget AddCommGroupCat.{u}).IsRightAdjoint
- instance : (forget GroupCat.{u}).IsRightAdjoint
- instance : (forget₂ (ModuleCat.{v} R) AddCommGroupCat.{v}).ReflectsIsomorphisms
- instance : (forget₂ CommGroupCat.{u} GroupCat.{u}).ReflectsIsomorphisms
- instance : Abelian AddCommGroupCat.{u}
- instance : Coe CommGroupCat.{u} CommMonCat.{u} where coe := (forget₂ CommGroupCat CommMonCat).obj
- instance : Coe CommGroupCat.{u} GroupCat.{u} where coe := (forget₂ CommGroupCat GroupCat).obj
- instance : Coe GroupCat.{u} MonCat.{u} where coe := (forget₂ GroupCat MonCat).obj
- instance : CoeSort CommGroupCat Type*
- instance : CoeSort GroupCat Type*
- instance : CoeSort GroupWithZeroCat Type*
- instance : CoeSort SemiNormedGroupCat Type*
- instance : CoeSort SemiNormedGroupCat₁ Type*
- instance : CoeSort SemigroupCat Type*
- instance : ConcreteCategory SemiNormedGroupCat := by
- instance : ConcreteCategory.{u} SemiNormedGroupCat₁
- instance : HasBinaryBiproducts AddCommGroupCat
- instance : HasCokernels SemiNormedGroupCat.{u}
- instance : HasCokernels SemiNormedGroupCat₁.{u}
- instance : HasColimitsOfSize.{0, 0} (AddCommGroupCat.{u}) := hasColimitsOfSize.{u, 0, 0}
- instance : HasColimitsOfSize.{u, u} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{v}
- instance : HasColimitsOfSize.{u, v} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u}
- instance : HasColimitsOfSize.{v, u} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u}
- instance : HasColimitsOfSize.{v, v} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u}
- instance : HasFiniteBiproducts AddCommGroupCat
- instance : HasForget₂ SemiNormedGroupCat₁ SemiNormedGroupCat
- instance : HasZeroObject CommGroupCat
- instance : HasZeroObject GroupCat
- instance : Inhabited (Action AddCommGroupCat G)
- instance : Inhabited CommGroupCat
- instance : Inhabited GroupCat
- instance : Inhabited GroupWithZeroCat
- instance : Inhabited SemiNormedGroupCat
- instance : Inhabited SemiNormedGroupCat₁
- instance : Inhabited SemigroupCat
- instance : LargeCategory.{u} GroupWithZeroCat
- instance : LargeCategory.{u} SemiNormedGroupCat₁
- instance : Limits.HasEqualizers.{u, u + 1} SemiNormedGroupCat
- instance : Limits.HasZeroMorphisms.{u, u + 1} SemiNormedGroupCat
- instance : Limits.HasZeroMorphisms.{u, u + 1} SemiNormedGroupCat₁
- instance : Preadditive AddCommGroupCat
- instance : Preadditive SemiNormedGroupCat.{u}
- instance : PreservesColimit F (forget₂ _ AddCommGroupCat)
- instance : Small.{u} (Functor.sections ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat))
- instance _root_.AddCommGroupCat.forgetPreservesLimits :
- instance {M N : GroupWithZeroCat} : FunLike (M ⟶ N) M N
- instance {M N : SemiNormedGroupCat} : Zero (M ⟶ N)
- instance {V W : SemiNormedGroupCat.{u}} : NNNorm (V ⟶ W)
- instance {V W : SemiNormedGroupCat.{u}} : Norm (V ⟶ W)
- instance {V W : SemiNormedGroupCat.{u}} : Sub (V ⟶ W)
- instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y
- instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y
- mulEquivIsoSemigroupCatIso
- semigroupCatIsoToMulEquiv
- toAddCommGroupCat
- toAddGroupCat
- toCommGroupCat
- toGroupCat
- wellPowered_addCommGroupCat
-+-+ adj
-+-+ comp_def
-+-+ concreteCategory
-+-+ enoughInjectives
-+-+ forgetPreservesLimits
-+-+ free
-+-+ hasColimitsOfShape
-+-+ hasColimitsOfSize
-+-+ hasLimits
-+-+ hasLimitsOfShape
-+-+ hasLimitsOfSize
-+-+ one_apply
-+-+ uliftFunctor
-+-+-+ colimit
-+-+-+ ext
-+-+-+-+ instFunLike
-+-+-+--++ coe_of
-+-+--++ isZero_of_subsingleton
-+-+--++ ofUnique
-+-+--++-+-+ of
-+--++ forget_map
-+--++--++ coe_comp
-+--++--++ coe_id
--++ cokernelCocone
--++ cokernelLift
--++ hasZeroObject
--++ toAddMonoidHomClass
--++ zero_apply

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>