From 8ebc1b0ebb7244f73ace1407ccb672a151c3a052 Mon Sep 17 00:00:00 2001
From: Petri Hienonen <petri.hienonen@gmail.com>
Date: Sun, 15 Feb 2026 15:59:37 +0200
Subject: Update

---
 SocietyCulture.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 SocietyCulture.lean

(limited to 'SocietyCulture.lean')

diff --git a/SocietyCulture.lean b/SocietyCulture.lean
new file mode 100644
index 0000000..ca4d0da
--- /dev/null
+++ b/SocietyCulture.lean
@@ -0,0 +1,17 @@
+import Mathematics
+
+-- Knowledge Base domain: SocietyCulture
+
+opaque Person : Type
+-- Person extends Entity
+axiom Person.val : Person → Entity
+opaque Place : Type
+-- Place extends Entity
+axiom Place.val : Place → Entity
+opaque City : Type
+-- City extends Place
+axiom City.val : City → Place
+opaque athens : City
+opaque birthyear : Person → Nat
+opaque bornIn : Person → Place → Prop
+axiom fact_bornIn_socrates_athens : bornIn socrates athens
-- 
cgit v1.3-1-g0d28