Isomorphisms of concrete groups
module group-theory.isomorphisms-concrete-groups where
Imports
open import category-theory.isomorphisms-large-precategories open import foundation.universe-levels open import group-theory.concrete-groups open import group-theory.precategory-of-concrete-groups
Idea
Isomorphisms of concrete groups are isomorphisms in the large precategory of concrete groups
Definition
iso-Concrete-Group : {l1 l2 : Level} → Concrete-Group l1 → Concrete-Group l2 → UU (l1 ⊔ l2) iso-Concrete-Group = iso-Large-Precategory Concrete-Group-Large-Precategory