Some refactorings

src/Algebra/Group/Aut.ard

@@ -25,4 +25,4 @@
   | * => ∘
   | ide-left => id-left
   | ide-right => id-right
-  | *-assoc => o-assoc
+  | *-assoc => o-assoc

src/Homotopy/EckmannHilton.ard

@@ -1,18 +1,9 @@
-\import Algebra.Group
-\import Arith.Nat
-\import Data.Bool
-\import Function
 \import Function.Meta
-\import HLevel
-\import Homotopy.Cube
-\import Homotopy.Hopf
 \import Homotopy.Loop
 \import Homotopy.Pointed \using  (Pointed \as HPointed)
 \import Meta
 \import Paths
 \import Paths.Meta
-\import Set
-
 
 {- | This is an algebraic formulation of Eckmann Hilton argument.
  - It is used, for example, to prove that a monoid object in category of monoids is commutative
@@ -108,7 +99,7 @@
       \func Relation2  : alp st2 bet = bet *> alp
         => rewrite (helper, pmap (\lam z => z *> alp) (LeftHorizontalWhiskering-relation bet), helper-2, idp_*>)idp
         \where {
-          \func helper : alp st2 bet = (LeftHorizontalWhiskering idp bet) *> alp => idp
+          \func helper : alp st2 bet = LeftHorizontalWhiskering idp bet *> alp => idp
           \func helper-2 : path (\lam _ => path (\lam _ => base {X})) = idp => idp
         }
 

src/Homotopy/Loop.ard

@@ -14,10 +14,8 @@
   | E => base = {X} base
   | base => idp
 
-\func Loop-Func {X Y : Pointed}(f : X ->* Y) : Loop X ->* Loop Y => (\lam z => (inv f.2) *> (pmap f.1 z) *> f.2, rewrite (f-of-idp f, idp_*>, inv_*>) idp)
-  \where {
-    \func f-of-idp {X Y : Pointed}(f : X ->* Y) : pmap {X} {Y} f.1 {X.base} {X.base} idp = idp => idp
-  }
+\func Loop-Func {X Y : Pointed} (f : X ->* Y) : Loop X ->* Loop Y
+  => (\lam z => inv f.2 *> pmap f.1 z *> f.2, pmap (_ *>) (idp_*> _) *> inv_*> _)
 
 \lemma loop-level {X : \Type}
                   (n : Nat)

src/Homotopy/Pointed.ard

@@ -31,5 +31,5 @@
   | ide => in0 X.base
 
 \func PointedTrunc0-Func {X Y : Pointed}(f : X ->* Y) : PointedHom (PointedTrunc0 X) (PointedTrunc0 Y) \cowith
-  | func => Trunc0.map' f.1
+  | func x => Trunc0.map x f.1
   | func-ide => rewrite f.2 idp

src/Set.ard

@@ -160,19 +160,7 @@
 
 \truncated \data Trunc0 (A : \Type) : \Set
   | in0 A
-  \where{
+  \where {
     \func map {A B : \Type} (t : Trunc0 A) (f : A -> B) : Trunc0 B \elim t
       | in0 a => in0 (f a)
-
-    \func map' {A B : \Type} (f : A -> B) (t : Trunc0 A) : Trunc0 B \elim t
-      | in0 a => in0 (f a)
-
-    \func map=map'{A B : \Type}(f : A -> B) (t : Trunc0 A) : map t f = map' f t \elim t
-      | in0 a => idp
-
-    \func t-exts {A B : \Type} {f g : A -> B}(p : f = g) : map' f = map' g => exts (\lam t => \case \elim t \with {
-      | in0 a => pmap in0 (path \lam i => (p i) a)
-    } )
-
-    \func t-exts'{A B : \Type} {f g : A -> B}(p : f = g) (a : Trunc0 A) : map' f a = map' g a => path (\lam i => (t-exts p i) a)
   }