diff --git a/pointed_binary.hlean b/pointed_binary.hlean
new file mode 100644
index 0000000..4a3b699
--- /dev/null
+++ b/pointed_binary.hlean
@@ -0,0 +1,164 @@
+/-
+Copyright (c) 2018 Ulrik Buchholtz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+
+import .pointed_pi
+
+open eq pointed equiv sigma is_equiv trunc option pi function fiber sigma.ops
+
+namespace pointed
+
+/- binary pointed maps -/
+structure bpmap (A B C : Type*) : Type :=
+  (f : A → B →* C)
+  (q : Πb, f pt b = pt)
+  (r : q pt = respect_pt (f pt))
+
+attribute [coercion] bpmap.f
+variables {A B C D A' B' C' : Type*} {f f' : bpmap A B C}
+definition respect_pt1 [unfold 4] (f : bpmap A B C) (b : B) : f pt b = pt :=
+bpmap.q f b
+
+definition respect_pt2 [unfold 4] (f : bpmap A B C) (a : A) : f a pt = pt :=
+respect_pt (f a)
+
+definition respect_ptpt [unfold 4] (f : bpmap A B C) : respect_pt1 f pt = respect_pt2 f pt :=
+bpmap.r f
+
+definition bpconst [constructor] (A B C : Type*) : bpmap A B C :=
+bpmap.mk (λa, pconst B C) (λb, idp) idp
+
+definition bppmap [constructor] (A B C : Type*) : Type* :=
+pointed.MK (bpmap A B C) (bpconst A B C)
+
+definition pmap_of_bpmap [constructor] (f : bppmap A B C) : ppmap A (ppmap B C) :=
+begin
+  fapply pmap.mk,
+  { intro a, exact pmap.mk (f a) (respect_pt2 f a) },
+  { exact eq_of_phomotopy (phomotopy.mk (respect_pt1 f) (respect_ptpt f)) }
+end
+
+definition bpmap_of_pmap [constructor] (f : ppmap A (ppmap B C)) : bppmap A B C :=
+begin
+  apply bpmap.mk (λa, f a) (ap010 pmap.to_fun (respect_pt f)),
+  exact respect_pt (phomotopy_of_eq (respect_pt f))
+end
+
+protected definition bpmap.sigma_char [constructor] (A B C : Type*) :
+  bpmap A B C ≃ Σ(f : A → B →* C) (q : Πb, f pt b = pt), q pt = respect_pt (f pt) :=
+begin
+  fapply equiv.MK,
+  { intro f, exact ⟨f, respect_pt1 f, respect_ptpt f⟩ },
+  { intro fqr, exact bpmap.mk fqr.1 fqr.2.1 fqr.2.2 },
+  { intro fqr, induction fqr with f qr, induction qr with q r, reflexivity },
+  { intro f, induction f, reflexivity }
+end
+
+definition to_homotopy_pt_square {f g : A →* B} (h : f ~* g) :
+  square (respect_pt f) (respect_pt g) (h pt) idp :=
+square_of_eq (to_homotopy_pt h)⁻¹
+
+definition bpmap_eq_equiv [constructor] (f f' : bpmap A B C):
+  f = f' ≃ Σ(h : Πa, f a ~* f' a) (q : Πb, square (respect_pt1 f b) (respect_pt1 f' b) (h pt b) idp), cube (vdeg_square (respect_ptpt f)) (vdeg_square (respect_ptpt f'))
+       vrfl ids
+       (q pt) (to_homotopy_pt_square (h pt)) :=
+begin
+  refine eq_equiv_fn_eq (bpmap.sigma_char A B C) f f' ⬝e _,
+  refine !sigma_eq_equiv ⬝e _, esimp,
+  refine sigma_equiv_sigma (!eq_equiv_homotopy ⬝e pi_equiv_pi_right (λa, !pmap_eq_equiv)) _,
+  intro h, exact sorry
+end
+
+definition bpmap_eq [constructor] (h : Πa, f a ~* f' a)
+  (q : Πb, square (respect_pt1 f b) (respect_pt1 f' b) (h pt b) idp)
+  (r : cube (vdeg_square (respect_ptpt f)) (vdeg_square (respect_ptpt f'))
+       vrfl ids
+       (q pt) (to_homotopy_pt_square (h pt))) : f = f' :=
+(bpmap_eq_equiv f f')⁻¹ᵉ ⟨h, q, r⟩
+
+definition pmap_equiv_bpmap [constructor] (A B C : Type*) : pmap A (ppmap B C) ≃ bpmap A B C :=
+begin
+  refine !pmap.sigma_char ⬝e _ ⬝e !bpmap.sigma_char⁻¹ᵉ,
+  refine sigma_equiv_sigma_right (λf, pmap_eq_equiv (f pt) !pconst) ⬝e _,
+  refine sigma_equiv_sigma_right (λf, !phomotopy.sigma_char)
+end
+
+definition pmap_equiv_bpmap' [constructor] (A B C : Type*) : pmap A (ppmap B C) ≃ bpmap A B C :=
+begin
+  refine equiv_change_fun (pmap_equiv_bpmap A B C) _,
+  exact bpmap_of_pmap, intro f, reflexivity
+end
+
+definition ppmap_pequiv_bppmap [constructor] (A B C : Type*) :
+  ppmap A (ppmap B C) ≃* bppmap A B C :=
+pequiv_of_equiv (pmap_equiv_bpmap' A B C) idp
+
+definition bpmap_functor [constructor] (f : A' →* A) (g : B' →* B) (h : C →* C')
+  (k : bpmap A B C) : bpmap A' B' C' :=
+begin
+  fapply bpmap.mk (λa', h ∘* k (f a') ∘* g),
+  { intro b', refine ap h _ ⬝ respect_pt h,
+    exact ap010 (λa b, k a b) (respect_pt f) (g b') ⬝ respect_pt1 k (g b') },
+  { apply whisker_right, apply ap02 h, esimp,
+    induction A with A a₀, induction B with B b₀, induction f with f f₀, induction g with g g₀,
+    esimp at *, induction f₀, induction g₀, esimp, apply whisker_left, exact respect_ptpt k },
+end
+
+definition bppmap_functor [constructor] (f : A' →* A) (g : B' →* B) (h : C →* C') :
+  bppmap A B C →* bppmap A' B' C' :=
+begin
+  apply pmap.mk (bpmap_functor f g h),
+  induction A with A a₀, induction B with B b₀, induction C' with C' c₀',
+  induction f with f f₀, induction g with g g₀, induction h with h h₀, esimp at *,
+  induction f₀, induction g₀, induction h₀,
+  reflexivity
+end
+
+  definition ppcompose_left' [constructor] (g : B →* C) : ppmap A B →* ppmap A C :=
+  pmap.mk (pcompose g)
+    begin induction C with C c₀, induction g with g g₀, esimp at *, induction g₀, reflexivity end
+
+  definition ppcompose_right' [constructor] (f : A →* B) : ppmap B C →* ppmap A C :=
+  pmap.mk (λg, g ∘* f)
+    begin induction B with B b₀, induction f with f f₀, esimp at *, induction f₀, reflexivity end
+
+definition ppmap_pequiv_bppmap_natural (f : A' →* A) (g : B' →* B) (h : C →* C') :
+  psquare (ppmap_pequiv_bppmap A B C) (ppmap_pequiv_bppmap A' B' C')
+          (ppcompose_right' f ∘* ppcompose_left' (ppcompose_right' g ∘* ppcompose_left' h))
+          (bppmap_functor f g h) :=
+begin
+  induction A with A a₀, induction B with B b₀, induction C' with C' c₀',
+  induction f with f f₀, induction g with g g₀, induction h with h h₀, esimp at *,
+  induction f₀, induction g₀, induction h₀,
+  fapply phomotopy.mk,
+  { intro k, fapply bpmap_eq,
+    { intro a, exact !passoc⁻¹* },
+    { intro b, apply vdeg_square, esimp,
+      refine ap02 _ !idp_con ⬝ _ ⬝ (ap (λx, ap010 pmap.to_fun x b) !idp_con)⁻¹ᵖ,
+      refine ap02 _ !ap_eq_ap010⁻¹ ⬝ !ap_compose' ⬝ !ap_compose ⬝ !ap_eq_ap010 },
+    { exact sorry }},
+  { exact sorry }
+end
+
+/- maybe this is useful for pointed naturality in C? -/
+definition ppmap_pequiv_bppmap_natural_right (h : C →* C') :
+  psquare (ppmap_pequiv_bppmap A B C) (ppmap_pequiv_bppmap A B C')
+          (ppcompose_left' (ppcompose_left' h))
+          (bppmap_functor !pid !pid h) :=
+begin
+  induction A with A a₀, induction B with B b₀, induction C' with C' c₀',
+  induction h with h h₀, esimp at *, induction h₀,
+  fapply phomotopy.mk,
+  { intro k, fapply bpmap_eq,
+    { intro a, exact pwhisker_left _ !pcompose_pid },
+    { intro b, apply vdeg_square, esimp,
+      refine ap02 _ !idp_con ⬝ _,
+      refine ap02 _ !ap_eq_ap010⁻¹ ⬝ !ap_compose' ⬝ !ap_compose ⬝ !ap_eq_ap010 },
+    { exact sorry }},
+  { exact sorry }
+end
+
+
+end pointed