diff --git a/.gitignore b/.gitignore
index 9abe79ec7..17195f116 100644
--- a/.gitignore
+++ b/.gitignore
@@ -23,4 +23,5 @@ CMakeFiles/
 doc/html
 make.deps
 src/emacs/dependencies
-compile_commands.json
\ No newline at end of file
+compile_commands.json
+*.hlean#
diff --git a/hott/cohomology/type_ab_functor.hlean b/hott/cohomology/type_ab_functor.hlean
new file mode 100644
index 000000000..e943fd696
--- /dev/null
+++ b/hott/cohomology/type_ab_functor.hlean
@@ -0,0 +1,36 @@
+/-
+Authors: Sayantan Khan
+
+Contravariant functors from (pointed?) Types to Abelian groups.
+-/
+
+import algebra.group algebra.homomorphism
+import types.pointed
+
+open algebra
+open sigma.ops
+open function
+open pointed
+
+structure type_ab_functor : Type :=
+  (fun_ty : Type → Type)
+  (target_ab : Π (A), add_ab_group(fun_ty(A)))
+  (fun_arr : Π {A B}, (A → B) → (Σ (f : fun_ty(B) → fun_ty(A)), is_add_hom(f)))
+  (respect_id : Π {A}, pr₁(fun_arr (@id A)) = id)
+  (respect_comp : Π {A B C}, Π (f : A → B), Π (g : B → C),
+    (pr₁(fun_arr (g ∘ f))) = ((pr₁ (fun_arr(f))) ∘ (pr₁ (fun_arr(g)))))
+
+attribute [coercion] type_ab_functor.fun_ty
+
+lemma extract_add : Π (A : Type), ab_group(A) → has_add(A) :=
+  λ A proofOfAbGroup, has_add.mk(algebra.ab_group.mul)
+
+structure Type_ab_functor : Type :=
+  (fun_ty : Type* → Type)
+  (target_ab : Π (A), add_ab_group(fun_ty(A)))
+  (fun_arr : Π {A B : Type*}, (A →* B) → (Σ (f : fun_ty(B) → fun_ty(A)), is_add_hom(f)))
+  (respect_id : Π {A}, pr₁(fun_arr (pid A)) = id)
+  (respect_comp : Π {A B C}, Π (f : A →* B), Π (g : B →* C),
+    (pr₁(fun_arr (g ∘* f))) = ((pr₁ (fun_arr(f))) ∘ (pr₁ (fun_arr(g)))))
+
+attribute [coercion] Type_ab_functor.fun_ty