diff --git a/homotopy/realprojective.hlean b/homotopy/realprojective.hlean
new file mode 100644
index 0000000..5c207f5
--- /dev/null
+++ b/homotopy/realprojective.hlean
@@ -0,0 +1,271 @@
+-- Based on Buchholtz-Rijke: Real projective spaces in HoTT
+-- Author: Ulrik Buchholtz
+
+import homotopy.join
+
+open eq nat susp pointed pmap sigma is_equiv equiv fiber is_trunc trunc
+  trunc_index is_conn sphere_index bool unit join pushout
+
+definition of_is_contr (A : Type) : is_contr A → A := @center A
+
+definition sigma_unit_left' [constructor] (B : unit → Type)
+   : (Σx, B x) ≃ B star :=
+begin
+  fapply equiv.MK,
+  { intro w, induction w with u b, induction u, exact b },
+  { intro b, exact ⟨ star, b ⟩ },
+  { intro b, reflexivity },
+  { intro w, induction w with u b, induction u, reflexivity }
+end
+
+definition sigma_eq_equiv' {A : Type} (B : A → Type)
+  (a₁ a₂ : A) (b₁ : B a₁) (b₂ : B a₂)
+  : (⟨a₁, b₁⟩ = ⟨a₂, b₂⟩) ≃ (Σ(p : a₁ = a₂), p ▸ b₁ = b₂) :=
+calc (⟨a₁, b₁⟩ = ⟨a₂, b₂⟩)
+    ≃ Σ(p : a₁ = a₂), b₁ =[p] b₂  : sigma_eq_equiv
+... ≃ Σ(p : a₁ = a₂), p ▸ b₁ = b₂ 
+ : by apply sigma_equiv_sigma_right; intro e; apply pathover_equiv_tr_eq
+
+definition dec_eq_is_prop [instance] (A : Type) : is_prop (decidable_eq A) :=
+begin
+  apply is_prop.mk, intros h k,
+  apply eq_of_homotopy, intro a,
+  apply eq_of_homotopy, intro b,
+  apply decidable.rec_on (h a b),
+  { intro p, apply decidable.rec_on (k a b),
+    { intro q, apply ap decidable.inl, apply is_set.elim },
+    { intro q, exact absurd p q } },
+  { intro p, apply decidable.rec_on (k a b),
+    { intro q, exact absurd q p },
+    { intro q, apply ap decidable.inr, apply is_prop.elim } }
+end
+
+definition dec_eq_bool : decidable_eq bool :=
+begin
+  intro a, induction a: intro b: induction b,
+  { exact decidable.inl idp },
+  { exact decidable.inr ff_ne_tt },
+  { exact decidable.inr (λ p, ff_ne_tt p⁻¹) },
+  { exact decidable.inl idp }
+end
+
+definition lemma_II_4 {A B : Type₀} (a : A) (b : B)
+  (e f : A ≃ B) (p : e a = b) (q : f a = b)
+  : (⟨e, p⟩ = ⟨f, q⟩) ≃ Σ (h : e ~ f), p = h a ⬝ q :=
+calc (⟨e, p⟩ = ⟨f, q⟩)
+    ≃ Σ (h : e = f), h ▸ p = q   : sigma_eq_equiv'
+... ≃ Σ (h : e ~ f), p = h a ⬝ q :
+begin
+  apply sigma_equiv_sigma ((equiv_eq_char e f) ⬝e eq_equiv_homotopy),
+  intro h, induction h, esimp, change (p = q) ≃ (p = idp ⬝ q),
+  rewrite idp_con
+end
+
+-- the type of two-element types
+structure BoolType :=
+  (carrier : Type₀)
+  (bool_eq_carrier : ∥ bool = carrier ∥)
+attribute BoolType.carrier [coercion]
+
+-- the basepoint
+definition pointed_BoolType [instance] : pointed BoolType :=
+pointed.mk (BoolType.mk bool (tr idp))
+
+definition pBoolType : pType := pType.mk BoolType pt
+
+definition BoolType.sigma_char : BoolType ≃ { X : Type₀ | ∥ bool = X ∥ } :=
+begin
+  fapply equiv.MK: intro Xf: induction Xf with X f,
+  { exact ⟨ X, f ⟩ }, { exact BoolType.mk X f },
+  { esimp }, { esimp }
+end
+
+definition BoolType.eq_equiv_equiv (A B : BoolType)
+  : (A = B) ≃ (A ≃ B) :=
+calc (A = B)
+    ≃ (BoolType.sigma_char A = BoolType.sigma_char B)
+    : eq_equiv_fn_eq_of_equiv
+... ≃ (BoolType.carrier A = BoolType.carrier B)
+    : begin
+        induction A with A p, induction B with B q,
+        symmetry, esimp, apply equiv_subtype 
+      end
+... ≃ (A ≃ B) : eq_equiv_equiv A B
+
+definition lemma_II_3 {A B : BoolType} (a : A) (b : B)
+  : (⟨A, a⟩ = ⟨B, b⟩) ≃ Σ (e : A ≃ B), e a = b :=
+calc (⟨A, a⟩ = ⟨B, b⟩)
+    ≃ Σ (e : A = B), e ▸ a = b : sigma_eq_equiv'
+... ≃ Σ (e : A ≃ B), e a = b   :
+    begin
+      apply sigma_equiv_sigma
+        (BoolType.eq_equiv_equiv A B),
+      intro e, induction e, unfold BoolType.eq_equiv_equiv,
+      induction A with A p, esimp
+    end
+
+definition theorem_II_2_lemma_1 (e : bool ≃ bool)
+  (p : e tt = tt) : e ff = ff :=
+sum.elim (dichotomy (e ff)) (λ q, q)
+begin
+  intro q, apply empty.elim, apply ff_ne_tt,
+  apply to_inv (eq_equiv_fn_eq_of_equiv e ff tt),
+  exact q ⬝ p⁻¹,
+end
+
+definition theorem_II_2_lemma_2 (e : bool ≃ bool)
+  (p : e tt = ff) : e ff = tt :=
+sum.elim (dichotomy (e ff))
+begin
+  intro q, apply empty.elim, apply ff_ne_tt,
+  apply to_inv (eq_equiv_fn_eq_of_equiv e ff tt),
+  exact q ⬝ p⁻¹
+end
+begin
+  intro q, exact q
+end
+
+definition theorem_II_2 : is_contr (Σ (X : BoolType), X) :=
+begin
+  fapply is_contr.mk,
+  { exact sigma.mk pt tt },
+  { intro w, induction w with Xf x, induction Xf with X f,
+    apply to_inv (lemma_II_3 tt x), apply of_is_contr,
+    induction f with f, induction f, induction x,
+    { apply is_contr.mk ⟨ equiv_bnot, idp ⟩,
+      intro w, induction w with e p, symmetry,
+      apply to_inv (lemma_II_4 tt ff e equiv_bnot p idp), 
+      fapply sigma.mk,
+      { intro b, induction b,
+        { exact theorem_II_2_lemma_2 e p },
+        { exact p } },
+      { reflexivity } },
+    { apply is_contr.mk ⟨ erfl, idp ⟩,
+      intro w, induction w with e p, symmetry,
+      apply to_inv (lemma_II_4 tt tt e erfl p idp),
+      fapply sigma.mk,
+      { intro b, induction b,
+        { exact theorem_II_2_lemma_1 e p },
+        { exact p } },
+      { reflexivity } } }
+end
+
+definition corollary_II_6 : Π A : BoolType, (pt = A) ≃ A :=
+@total_space_method BoolType pt BoolType.carrier theorem_II_2 idp
+
+definition is_conn_BoolType [instance] : is_conn 0 BoolType :=
+begin
+  apply is_contr.mk (tr pt),
+  intro X, induction X with X, induction X with X p,
+  induction p with p, induction p, reflexivity
+end
+
+definition bool_of_two (A : BoolType) (x y : A) : bool :=
+to_inv (BoolType.eq_equiv_equiv pt A
+  (to_inv (corollary_II_6 A) x)) y
+
+definition bool_type_dec_eq : Π (A : BoolType), decidable_eq A :=
+@is_conn.is_conn.elim -1 pBoolType is_conn_BoolType
+    (λ A : BoolType, decidable_eq A) _ dec_eq_bool
+
+definition alpha (A : BoolType) (x y : A) : bool :=
+decidable.rec_on (bool_type_dec_eq A x y)
+    (λ p, tt) (λ q, ff)
+
+definition alpha_inv (a b : bool) : alpha pt a (alpha pt a b) = b :=
+begin
+  induction a: induction b: esimp
+end
+
+definition is_equiv_alpha [instance] : Π {A : BoolType} (a : A),
+  is_equiv (alpha A a) :=
+begin
+  apply @is_conn.elim -1 pBoolType is_conn_BoolType
+    (λ A : BoolType, Π a : A, is_equiv (alpha A a)),
+  intro a,
+  exact adjointify (alpha pt a) (alpha pt a) (alpha_inv a) (alpha_inv a)
+end
+
+definition alpha_equiv (A : BoolType) (a : A) : A ≃ bool :=
+equiv.mk (alpha A a) (is_equiv_alpha a)
+
+definition alpha_symm : Π (A : BoolType) (x y : A),
+  alpha A x y = alpha A y x :=
+begin
+  apply @is_conn.elim -1 pBoolType is_conn_BoolType
+    (λ A : BoolType, Π x y : A, alpha A x y = alpha A y x),
+  intros x y, induction x: induction y: esimp
+end
+
+-- we define the type of types together with a line bundle
+structure two_cover :=
+  (carrier : Type₀)
+  (cov : carrier → Type₀)
+  (cov_eq : Π x : carrier, ∥ bool = cov x ∥ )
+open two_cover
+
+definition empty_two_cover : two_cover :=
+two_cover.mk empty empty.elim (empty.rec _)
+
+open sigma.ops
+
+definition two_cover_step (X : two_cover) : two_cover :=
+begin
+  fapply two_cover.mk,
+  { exact pushout (@sigma.pr1 (carrier X) (cov X)) (λ x, star) },
+  { fapply pushout.elim_type,
+    { intro x, exact cov X x },
+    { intro u, exact BoolType.carrier pt },
+    { intro w, exact alpha_equiv
+        (BoolType.mk (cov X w.1) (cov_eq X w.1)) w.2 } },
+  { fapply pushout.rec,
+    { intro x, exact cov_eq X x },
+    { intro u, exact tr idp },
+    { intro w, apply is_prop.elimo } }
+end
+
+definition realprojective_two_cover : ℕ₋₁ → two_cover :=
+sphere_index.rec empty_two_cover (λ x, two_cover_step)
+
+definition realprojective : ℕ₋₁ → Type₀ :=
+λ n, carrier (realprojective_two_cover n)
+
+definition realprojective_cov [reducible] (n : ℕ₋₁)
+  : realprojective n → BoolType :=
+λ x, BoolType.mk
+  (cov (realprojective_two_cover n) x)
+  (cov_eq (realprojective_two_cover n) x)
+
+definition theorem_III_3_u [reducible] (n : ℕ₋₁)
+  : (Σ (w : Σ x, realprojective_cov n x), realprojective_cov n w.1)
+  ≃ (Σ x, realprojective_cov n x) × bool :=
+calc  (Σ (w : Σ x, realprojective_cov n x), realprojective_cov n w.1)
+    ≃ (Σ (w : Σ x, realprojective_cov n x), realprojective_cov n w.1)
+  : sigma_assoc_comm_equiv
+... ≃ Σ (w : Σ x, realprojective_cov n x), bool
+  : @sigma_equiv_sigma_right (Σ x : realprojective n, realprojective_cov n x)
+      (λ w, realprojective_cov n w.1) (λ w, bool)
+      (λ w, alpha_equiv (realprojective_cov n w.1) w.2)
+... ≃ (Σ x, realprojective_cov n x) × bool
+  : equiv_prod
+
+definition theorem_III_3 (n : ℕ₋₁)
+  : sphere n ≃ sigma (realprojective_cov n) :=
+begin
+  induction n with n IH,
+  { symmetry, apply sigma_empty_left },
+  { apply equiv.trans (join.bool (sphere n))⁻¹ᵉ,
+    apply equiv.trans (join.equiv_closed erfl IH),
+    symmetry, refine equiv.trans _ !join.symm,
+    apply equiv.trans !pushout.flattening, esimp,
+    fapply pushout.equiv,
+    { unfold function.compose, exact theorem_III_3_u n},
+    { reflexivity },
+    { exact sigma_unit_left' (λ u, bool) },
+    { unfold function.compose, esimp, intro w,
+      induction w with w z, induction w with x y,
+      reflexivity },
+    { unfold function.compose, esimp, intro w,
+      induction w with w z, induction w with x y,
+      exact alpha_symm (realprojective_cov n x) y z } }
+end