From 09c6cbe434bcd54d55256a8ac84b70a5c24365c9 Mon Sep 17 00:00:00 2001
From: 5HT <maxim@synrc.com>
Date: Sun, 3 Mar 2024 20:03:55 +0200
Subject: [PATCH] pythagor

---
 lib/foundations/logic/hilbert.anders     | 12 +++++++++---
 lib/foundations/mltt/mltt.anders         |  3 ++-
 lib/foundations/mltt/vec.anders          |  2 +-
 lib/mathematics/geometry/pythagor.anders | 15 +++++++++++++++
 4 files changed, 27 insertions(+), 5 deletions(-)
 create mode 100644 lib/mathematics/geometry/pythagor.anders

diff --git a/lib/foundations/logic/hilbert.anders b/lib/foundations/logic/hilbert.anders
index 5e02025d..a95fe6f2 100644
--- a/lib/foundations/logic/hilbert.anders
+++ b/lib/foundations/logic/hilbert.anders
@@ -22,16 +22,22 @@ def e₁ : E := \ (p : Ω) (x: p.1), s p p p (k p p) (k p p x) x
 
 def X
  := Π (p q r x y z h w: Ω)
-      (k: (p.1 → q.1 → p.1) → ((x.1 → y.1 → z.1) → (x.1 → y.1) → x.1 → z.1) → (r.1 → w.1 → r.1) → h.1), h.1
+      (k: (p.1 → q.1 → p.1) →
+          ((x.1 → y.1 → z.1) → (x.1 → y.1) → x.1 → z.1) →
+          (r.1 → w.1 → r.1) → h.1), h.1
 
 def x : X
  := \ (p q r a b c h w: Ω)
-      (v: (p.1 → q.1 → p.1) → ((a.1 → b.1 → c.1) → (a.1 → b.1) → a.1 → c.1) → (r.1 → w.1 → r.1) → h.1),
+      (v: (p.1 → q.1 → p.1) →
+          ((a.1 → b.1 → c.1) → (a.1 → b.1) → a.1 → c.1) →
+          (r.1 → w.1 → r.1) → h.1),
       v (k p q) (s a b c) (k r w)
 
 def x₁ : X
  := \ (p q r x y z h w: Ω)
-      (v: (p.1 → q.1 → p.1) → ((x.1 → y.1 → z.1) → (x.1 → y.1) → x.1 → z.1) → (r.1 → w.1 → r.1) → h.1),
+      (v: (p.1 → q.1 → p.1) →
+          ((x.1 → y.1 → z.1) → (x.1 → y.1) → x.1 → z.1) →
+          (r.1 → w.1 → r.1) → h.1),
       v (\ (x: p.1) (y: q.1), x)
         (\ (a: x.1 → y.1 → z.1) (b: x.1 → y.1) (c: x.1), a c (b c))
         (\ (e: r.1) (f: w.1), e)
diff --git a/lib/foundations/mltt/mltt.anders b/lib/foundations/mltt/mltt.anders
index ced9f018..cffe9699 100644
--- a/lib/foundations/mltt/mltt.anders
+++ b/lib/foundations/mltt/mltt.anders
@@ -59,7 +59,8 @@ def MLTT (A : U) : U₁ ≔
     (=-form  : Π (a : A), A → U)
     (=-ctor₁ : Π (a : A), Path A a a)
     (=-elim₁ : Π (a : A) (C: D A) (d: C a a (=-ctor₁ a)) (y: A) (p: Path A a y), C a y p)
-    (=-comp₁ : Π (a : A) (C: D A) (d: C a a (=-ctor₁ a)), Path (C a a (=-ctor₁ a)) d (=-elim₁ a C d a (=-ctor₁ a))), 𝟏
+    (=-comp₁ : Π (a : A) (C: D A) (d: C a a (=-ctor₁ a)),
+               Path (C a a (=-ctor₁ a)) d (=-elim₁ a C d a (=-ctor₁ a))), 𝟏
 
 --- Self-aware MLTT:
 --- Theorem. Id β-rule is derivable from generalized transport
diff --git a/lib/foundations/mltt/vec.anders b/lib/foundations/mltt/vec.anders
index 7cb2dfb5..ece22a8d 100644
--- a/lib/foundations/mltt/vec.anders
+++ b/lib/foundations/mltt/vec.anders
@@ -31,4 +31,4 @@ def Vec-rec (A B : U) (z : B) (s : Π (n : ℕ), A → Vec A n → B → B) (m :
 def Vec-map (A B : U) (f : A → B) (n : ℕ)
   : Vec A n → Vec B n
  := Vec-ind A (λ (k : ℕ) (_ : Vec A k), Vec B k) ★ (λ (k : ℕ)
-              (x : A) (_ : Vec A k), vsucc B k (f x)) n
+                 (x : A) (_ : Vec A k), vsucc B k (f x)) n
diff --git a/lib/mathematics/geometry/pythagor.anders b/lib/mathematics/geometry/pythagor.anders
new file mode 100644
index 00000000..8784b9c8
--- /dev/null
+++ b/lib/mathematics/geometry/pythagor.anders
@@ -0,0 +1,15 @@
+module pythagor where
+
+def pred (A: U) := A -> U
+def relx (A: U) (R : A -> A -> U) (P : pred A) (x: A) : U := Π (y : A), R y x -> P y
+def domain (A : U) (R : A -> A -> U) (P : pred A) : U := Π (x: A), (relx A R P x) -> P x
+def codom (A : U) (P : pred A) : U := Π (x : A), P x
+def noether (A : U) (R : A -> A -> U) : U₁ := Π (P: pred A), domain A R P -> codom A P
+def not (A: U) : U := A -> 𝟎
+def prime (A: U) := ? -- \ (x: A), ...
+def multiple (A: U) (R : A -> A -> U) (P : pred A) (x: A) : A -> A -> U := ? -- \ (x y: A), A
+def isNotSquare (A: U) (R : A -> A -> U) (P : pred A) (x: A) : pred A := ? -- \ (x: A), A
+
+theorem Sq2 (A: U) (R : A -> A -> U) (P : A -> U) (x : A)
+  : prime A -> noether A (multiple A R P x) -> isNotSquare A R P x
+ := ?