Mere equivalences of concrete group actions
module group-theory.mere-equivalences-concrete-group-actions where
Imports
open import foundation.functoriality-propositional-truncation open import foundation.mere-equality open import foundation.propositional-truncations open import foundation.propositions open import foundation.universe-levels open import group-theory.concrete-group-actions open import group-theory.concrete-groups open import group-theory.equivalences-concrete-group-actions
Definition
mere-equiv-action-Concrete-Group-Prop : {l1 l2 l3 : Level} (G : Concrete-Group l1) → action-Concrete-Group l2 G → action-Concrete-Group l3 G → Prop (l1 ⊔ l2 ⊔ l3) mere-equiv-action-Concrete-Group-Prop G X Y = trunc-Prop (equiv-action-Concrete-Group G X Y) mere-equiv-action-Concrete-Group : {l1 l2 l3 : Level} (G : Concrete-Group l1) → action-Concrete-Group l2 G → action-Concrete-Group l3 G → UU (l1 ⊔ l2 ⊔ l3) mere-equiv-action-Concrete-Group G X Y = type-Prop (mere-equiv-action-Concrete-Group-Prop G X Y) is-prop-mere-equiv-action-Concrete-Group : {l1 l2 l3 : Level} (G : Concrete-Group l1) (X : action-Concrete-Group l2 G) (Y : action-Concrete-Group l3 G) → is-prop (mere-equiv-action-Concrete-Group G X Y) is-prop-mere-equiv-action-Concrete-Group G X Y = is-prop-type-Prop (mere-equiv-action-Concrete-Group-Prop G X Y) refl-mere-equiv-action-Concrete-Group : {l1 l2 : Level} (G : Concrete-Group l1) (X : action-Concrete-Group l2 G) → mere-equiv-action-Concrete-Group G X X refl-mere-equiv-action-Concrete-Group G X = unit-trunc-Prop (id-equiv-action-Concrete-Group G X)
Properties
Mere equivalences of concrete group actions give mere equalities
mere-eq-mere-equiv-action-Concrete-Group : {l1 l2 : Level} (G : Concrete-Group l1) (X : action-Concrete-Group l2 G) (Y : action-Concrete-Group l2 G) → mere-equiv-action-Concrete-Group G X Y → mere-eq X Y mere-eq-mere-equiv-action-Concrete-Group G X Y = map-trunc-Prop (eq-equiv-action-Concrete-Group G X Y)