File tree Expand file tree Collapse file tree 1 file changed +6
-6
lines changed
src/Algebra/Construct/Quotient Expand file tree Collapse file tree 1 file changed +6
-6
lines changed Original file line number Diff line number Diff line change @@ -108,11 +108,11 @@ quotientGroup = record { isGroup = quotientIsGroup }
108108_/_ : Group c (c ⊔ ℓ ⊔ c′)
109109_/_ = quotientGroup
110110
111- project : Group.Carrier G → Group.Carrier quotientGroup
112- project x = x -- because we do all the work in the relation
111+ π : Group.Carrier G → Group.Carrier quotientGroup
112+ π x = x -- because we do all the work in the relation
113113
114- project -isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) project
115- project -isHomomorphism = record
114+ π -isHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) π
115+ π -isHomomorphism = record
116116 { isMonoidHomomorphism = record
117117 { isMagmaHomomorphism = record
118118 { isRelHomomorphism = record
@@ -125,5 +125,5 @@ project-isHomomorphism = record
125125 ; ⁻¹-homo = λ _ → ≋-refl
126126 }
127127
128- project -surjective : Surjective _≈_ _≋_ project
129- project -surjective g = g , ≈⇒≋
128+ π -surjective : Surjective _≈_ _≋_ π
129+ π -surjective g = g , ≈⇒≋
You can’t perform that action at this time.
0 commit comments