diff --git a/pyoneda.hlean b/pyoneda.hlean
new file mode 100644
index 0000000..c96d572
--- /dev/null
+++ b/pyoneda.hlean
@@ -0,0 +1,111 @@
+/-
+In this file we give a consequence of the Yoneda lemma for pointed types which we can state
+internally. If we have a pointed equivalence α : A ≃* B, we can turn it into an equivalence
+γ : (B →* X) ≃* (A →* X), natural in X. Naturality means that if we have f : X → X' then we
+can fill the following square (using a pointed homotopy)
+(B →* X)  --> (A →* X)
+   |             |
+   v             v
+(B →* X') --> (B →* X')
+such that if f is the constant map, then this square is equal to the canonical filler of that
+square (where the fact that f is constant is used).
+
+Conversely, if we have such a γ natural in X, we can obtain an equivalence A ≃* B.
+Moreover, these operations are equivalences in the sense that going from α to γ to α is the
+same as doing nothing, and going from γ to α to γ is the same as doing nothing. However, we
+need higher coherences for γ to show that the proof of naturality is the same, which we didn't do.
+
+Author: Floris van Doorn (informal proofs in collaboration with Stefano Piceghello)
+-/
+
+import .pointed
+
+open equiv is_equiv eq
+namespace pointed
+
+  universe variable u
+
+  definition ppcompose_right_ppcompose_left {A A' B B' : Type*} (f : A →* A') (g : B →* B'):
+    psquare (ppcompose_right f) (ppcompose_right f) (ppcompose_left g) (ppcompose_left g) :=
+  ptranspose !ppcompose_left_ppcompose_right
+
+  -- definition pyoneda₂ {A B : pType.{u}} (γ : Π(X : pType.{u}), ppmap B X ≃* ppmap A X)
+  --   (p : Π(X X' : Type*), _ ∘* pppcompose B X X' ~* (_ : ppmap _ _))
+  --   : A ≃* B :=
+  -- begin
+  --   fapply pequiv.MK,
+  --   { exact γ B (pid B) },
+  --   { exact (γ A)⁻¹ᵉ* (pid A) },
+  --   { refine phomotopy_of_eq (p _ _) ⬝* _,
+  --     exact pap (γ A) !pcompose_pid ⬝* phomotopy_of_eq (to_right_inv (γ A) _) },
+  --   { refine phomotopy_of_eq ((p _)⁻¹ʰ* _) ⬝* _,
+  --     exact pap (γ B)⁻¹ᵉ* !pcompose_pid ⬝* phomotopy_of_eq (to_left_inv (γ B) _) }
+  -- end
+
+-- print ⁻¹ʰᵗʸʰ
+-- print eq.hhinverse
+  definition pyoneda_weak {A B : pType.{u}} (γ : Π(X : pType.{u}), ppmap B X ≃* ppmap A X)
+    (p : Π⦃X X' : Type*⦄ (f : X →* X') (g : B →* X), f ∘* γ X g ~* γ X' (f ∘* g)) : A ≃* B :=
+  begin
+    fapply pequiv.MK,
+    { exact γ B (pid B) },
+    { exact (γ A)⁻¹ᵉ* (pid A) },
+    { refine p _ _ ⬝* _,
+      exact pap (γ A) !pcompose_pid ⬝* phomotopy_of_eq (to_right_inv (γ A) _) },
+    { -- refine (p _)⁻¹ʰᵗʸʰ _ ⬝* _,
+      -- exact pap (γ B)⁻¹ᵉ* !pcompose_pid ⬝* phomotopy_of_eq (to_left_inv (γ B) _)
+      exact sorry
+      }
+  end
+
+  definition pyoneda {A B : pType.{u}} (γ : Π(X : pType.{u}), ppmap B X ≃* ppmap A X)
+    (p : Π⦃X X' : Type*⦄ (f : X →* X'), psquare (γ X) (γ X') (ppcompose_left f) (ppcompose_left f))
+    : A ≃* B :=
+--  pyoneda_weak γ p
+  begin
+    fapply pequiv.MK,
+    { exact γ B (pid B) },
+    { exact (γ A)⁻¹ᵉ* (pid A) },
+    { refine phomotopy_of_eq (p _ _) ⬝* _,
+      exact pap (γ A) !pcompose_pid ⬝* phomotopy_of_eq (to_right_inv (γ A) _) },
+    { refine phomotopy_of_eq ((p _)⁻¹ʰ* _) ⬝* _,
+      exact pap (γ B)⁻¹ᵉ* !pcompose_pid ⬝* phomotopy_of_eq (to_left_inv (γ B) _) }
+  end
+
+  definition pyoneda_right_inv {A B : pType.{u}} (α : A ≃* B) :
+    pyoneda (λX, ppmap_pequiv_ppmap_left α) (λX X' f, proof !ppcompose_right_ppcompose_left qed) ~*
+    α :=
+  phomotopy.mk homotopy.rfl idp
+
+  definition pyoneda_left_inv {A B : pType.{u}} (γ : Π(X : pType.{u}), ppmap B X ≃* ppmap A X)
+    (p : Π⦃X X' : Type*⦄ (f : X →* X'), psquare (γ X) (γ X') (ppcompose_left f) (ppcompose_left f))
+    (H : Π⦃X⦄ (X' : Type*) (g : B →* X), phomotopy_of_eq (p (pconst X X') g) =
+      !pconst_pcompose ⬝* (pap (γ X') !pconst_pcompose ⬝* phomotopy_of_eq (respect_pt (γ X')))⁻¹*)
+    (X : Type*) : ppcompose_right (pyoneda γ p) ~* γ X :=
+ begin
+    fapply phomotopy_mk_ppmap,
+    { intro f, refine phomotopy_of_eq (p _ _) ⬝* _, exact pap (γ X) !pcompose_pid },
+    { refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
+      refine !trans_assoc ⬝ _,
+      refine H X (pid B) ◾** idp ⬝ !trans_assoc ⬝ idp ◾** _ ⬝ !trans_refl,
+      apply trans_left_inv }
+  end
+
+  definition pyoneda_weak_left_inv {A B : pType.{u}} (γ : Π(X : pType.{u}), ppmap B X ≃* ppmap A X)
+    (p : Π⦃X : Type*⦄ (X' : Type*) (g : B →* X), ppcompose_right (γ X g) ~* γ X' ∘* ppcompose_right g)
+    (X : Type*) : ppcompose_right (pyoneda_weak γ (λX X' f g, phomotopy_of_eq (p X' g f))) ~* γ X :=
+  begin
+    fapply phomotopy_mk_ppmap,
+    { intro f, refine phomotopy_of_eq (p _ _ _) ⬝* _, exact pap (γ X) !pcompose_pid },
+    { refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
+      refine !trans_assoc ⬝ _,
+      refine (ap phomotopy_of_eq (eq_con_inv_of_con_eq (to_homotopy_pt (p X (pid B)))) ⬝
+        !phomotopy_of_eq_con ⬝ !phomotopy_of_eq_of_phomotopy ◾**
+        (!phomotopy_of_eq_inv ⬝ (!phomotopy_of_eq_con ⬝ (!phomotopy_of_eq_ap ⬝
+        ap (pap' _) !phomotopy_of_eq_of_phomotopy) ◾** idp)⁻²**)) ◾** idp ⬝ _,
+      refine !trans_assoc ⬝ idp ◾** _ ⬝ !trans_refl,
+      apply trans_left_inv }
+  end
+
+
+end pointed