From 56cd88267c5154c2bc27f1533932392a97c67eeb Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Mon, 25 Jan 2016 16:54:24 +0000
Subject: [PATCH] feat(hott): add cofiber of a function, prove lemma that
 cofibers of equivalences are contractible

---
 hott/homotopy/cofiber.hlean | 40 +++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 hott/homotopy/cofiber.hlean

diff --git a/hott/homotopy/cofiber.hlean b/hott/homotopy/cofiber.hlean
new file mode 100644
index 0000000000..14961d17d9
--- /dev/null
+++ b/hott/homotopy/cofiber.hlean
@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2016 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jakob von Raumer
+
+The Cofiber Type
+-/
+import hit.pointed_pushout function
+
+open eq pushout unit pointed is_trunc is_equiv
+
+definition cofiber {A B : Type} (f : A → B) := pushout (λ (a : A), ⋆) f
+
+namespace cofiber
+  section
+  parameters {A B : Type} (f : A → B)
+
+  protected definition base : cofiber f := inl ⋆
+
+  protected definition cod : B → cofiber f := inr
+
+  protected definition contr_of_equiv [H : is_equiv f] : is_contr (cofiber f) :=
+  begin
+    fapply is_contr.mk, exact base,
+    intro a, induction a with [u, b],
+    { cases u, reflexivity },
+    { exact !glue ⬝ ap inr (right_inv f b) },
+    { apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, refine !ap_constant ⬝ph _, 
+      esimp, krewrite adj, apply move_bot_of_left, krewrite idp_con, 
+      apply transpose, refine _ ⬝hp !ap_compose, apply square_Flr_idp_ap },
+  end
+
+  end
+end cofiber
+
+-- Pointed version
+
+definition Cofiber {A B : Type*} (f : A →* B) : Type* := Pushout (pconst A Unit) f
+
+