diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean
index 2fd2ff8..15853ff 100644
--- a/algebra/arrow_group.hlean
+++ b/algebra/arrow_group.hlean
@@ -1,7 +1,11 @@
-/- various groups of maps. Most importantly we define a group structure on trunc 0 (A →* Ω B),
-   which is used in the definition of cohomology -/
+/-
+Copyright (c) 2016-2017 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Ulrik Buchholtz
 
---author: Floris van Doorn
+Various groups of maps. Most importantly we define a group structure
+on trunc 0 (A →* Ω B), which is used in the definition of cohomology.
+-/
 
 import algebra.group_theory ..pointed ..pointed_pi eq2 homotopy.susp
 open pi pointed algebra group eq equiv is_trunc trunc susp
diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean
index fb07352..cb6e3c7 100644
--- a/homotopy/cohomology.hlean
+++ b/homotopy/cohomology.hlean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2016 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
+Authors: Floris van Doorn, Ulrik Buchholtz
 
 Reduced cohomology of spectra and cohomology theories
 -/
diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index 8d5017a..6b95c84 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -1,3 +1,11 @@
+/-
+Copyright (c) 2017 Floris van Doorn and Ulrik Buchholtz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Ulrik Buchholtz
+
+Truncatedness and truncation of spectra
+-/
+
 import .spectrum .EM
 
 namespace int