From b177e659535788aefd5df7ab630ae34f83832ce0 Mon Sep 17 00:00:00 2001
From: Ramkumar Ramachandra <r@artagnon.com>
Date: Sat, 12 Oct 2024 13:18:29 +0100
Subject: [PATCH] LeYoneda: clean detritus; polish README

---
 README.md                          | 10 ++++------
 "theories/\316\275Type/LeYoneda.v" | 16 ----------------
 2 files changed, 4 insertions(+), 22 deletions(-)

diff --git a/README.md b/README.md
index c7bb5a4..97b8d8b 100644
--- a/README.md
+++ b/README.md
@@ -13,13 +13,11 @@ Some features of this project:
 
 Our axioms are:
 
-```text
-Section Variables:
-side : HSet
+```coq
 Axioms:
-functional_extensionality_dep
-  : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
-	(forall x : A, f x = g x) -> f = g
+  functional_extensionality_dep
+    : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
+      (forall x : A, f x = g x) -> f = g
 ```
 
 ## Current status
diff --git "a/theories/\316\275Type/LeYoneda.v" "b/theories/\316\275Type/LeYoneda.v"
index 67f4f3e..0bbba03 100644
--- "a/theories/\316\275Type/LeYoneda.v"
+++ "b/theories/\316\275Type/LeYoneda.v"
@@ -353,20 +353,4 @@ Ltac solve_leY :=
   | [ |- ?c ] => debug ltac:(idtac "Not a leY:" c); fail
   end.
 
-Example ex1 (n p q r : nat)
-  (Hpr : p.+2 <= r.+2)
-  (Hrq : r.+2 <= q.+2)
-  (Hq : q.+2 <= n) : forall C, (p.+1 <= q.+2 -> p.+1 <= q.+1 -> p.+2 <= r.+2 -> p.+2 <= n -> C) -> C.
-intros C H. apply H.
-solve_leY.
-solve_leY.
-solve_leY.
-solve_leY.
-Qed.
-
 Hint Extern 0 (leY _ _) => solve_leY : typeclass_instances.
-
-Example ex2 {n} p q r {Hpr : p.+2 <= r.+2} {Hrq : r.+2 <= q.+2} {Hq : q.+2 <= n}
-  {H: forall p q r, p.+1 <= r.+1 -> r <= q -> q <= n -> p <= n}: p <= n.
-  now apply (H p q r _ _ _).
-Qed.