Mere equivalences of group actions
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-03-17.
Last modified on 2023-03-10.
module group-theory.mere-equivalences-group-actions where
Imports
open import foundation.propositional-truncations open import foundation.propositions open import foundation.universe-levels open import group-theory.equivalences-group-actions open import group-theory.group-actions open import group-theory.groups
Definition
module _ {l1 l2 l3 : Level} (G : Group l1) (X : Abstract-Group-Action G l2) (Y : Abstract-Group-Action G l3) where mere-equiv-Abstract-Group-Action-Prop : Prop (l1 ⊔ l2 ⊔ l3) mere-equiv-Abstract-Group-Action-Prop = trunc-Prop (equiv-Abstract-Group-Action G X Y) mere-equiv-Abstract-Group-Action : UU (l1 ⊔ l2 ⊔ l3) mere-equiv-Abstract-Group-Action = type-Prop mere-equiv-Abstract-Group-Action-Prop
Recent changes
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).