fph

lib/foundations/mltt/nat.anders

@@ -38,6 +38,11 @@ def two : ℕ := succ one
 def three : ℕ := succ two
 def four : ℕ := succ three
 def five : ℕ := succ four
+def six : ℕ := succ five
+def seven : ℕ := succ six
+def eight : ℕ := succ seven
+def nine : ℕ := succ eight
+def ten : ℕ := succ nine
 
 def 5′ : ℕ := plus two three
 def 10′ : ℕ := mult 5′ two

lib/foundations/univalent/equiv.anders

@@ -70,10 +70,15 @@ def hcomp-Glue' (A : U) (φ : I)
 
 --- Equiv as [Right] Identity System [Escardó] 2014
 
+--- def singl (A: U) (a: A): U := Σ (x: A), Path A a x
+--- def isContr (A: U) : U := Σ (x: A), Π (y: A), Path A x y
+--- def contr (A : U) (a b : A) (p : Path A a b) : Path (singl A a) (eta A a) (b, p) := <i> (p @ i, <j> p @ i /\ j)
+--- def isContrSingl (A : U) (a : A) : isContr (singl A a) := ((a,idp A a),(\ (z:singl A a), contr A a z.1 z.2))
+
 def single (A : U) : U := Σ (B: U), equiv A B
 def single2 (A : U) : U := Σ (B: U), equiv B A
 axiom contrEquiv (A B : U) (p : equiv A B) : Path (single A) (A,idEquiv A) (B,p)
--- := <i> ((univ-intro B A p) @ i, <j> univ-intro B A p @ i /\ j)
+-- := (<i> ((univ-intro A B p) @ i, <j> univ-intro A B p @ i /\ j))
 def EquivIsContr (A: U) : isContr (single A) := ((A, idEquiv A), \(z:single A), (contrEquiv A z.1 z.2))
 def isContr→isProp (A: U) (w: isContr A) (a b : A) : Path A a b
  := <i> hcomp A (∂ i) (λ (j : I), [(i = 0) → a, (i = 1) → (w.2 b) @ j]) ((<i4> w.2 a @ -i) @ i)

lib/mathematics/categories/meta/mipham.anders

@@ -0,0 +1,76 @@
+module mipham where
+import lib/foundations/mltt/vec
+option irrelevance true
+
+--- Формальна філософія
+--- Theories Index
+
+def Eye   : U := unit -- 01 -- Гедоністичний (rab tu dga’ ba).
+def Ear   : U := unit -- 02 -- Міцний (dri ma med pa).
+def Nose  : U := unit -- 03 -- Ілюмінуючий (’od byed pa).
+def Mouth : U := unit -- 04 -- Радіантний (’od ’phro can).
+def Body  : U := unit -- 05 -- Незворотній (shin tu sbyang dka’ ba).
+def Sems  : U := unit -- 06 -- Ясний (mngon du gyur ba).
+def Nyid3 : U := unit -- 07 -- Прогресуючий (ring du song ba).
+def Nyid2 : U := unit -- 08 -- Непорушний (mi gyo ba).
+def Nyid1 : U := unit -- 09 -- Неперевершений (legs pa’i blo gros).
+def Nyid0 : U := unit -- 10 -- Хмари Дхарми (chos kyi sprin).
+
+def nyid3 : Vec U zero := star
+
+def HomotopyTheory       : U := unit
+def HomologicalAlgebra   : U := unit
+def AlgebraicGeometry    : U := unit
+def DifferentialGeometry : U := unit
+def SuperGeometry        : U := unit
+
+def nyid2 : Vec U five
+ := vsucc U four HomotopyTheory
+  ( vsucc U three HomologicalAlgebra
+  ( vsucc U two AlgebraicGeometry
+  ( vsucc U one DifferentialGeometry
+  ( vsucc U zero SuperGeometry
+  ( vzero U )))))
+
+def Abelian   : U := unit
+def Derived   : U := unit
+def Model     : U := unit
+def Spectra   : U := unit
+def T-Spectra : U := unit
+def Yogas     : U := unit
+
+def nyid1 : Vec U six
+ := vsucc U five Abelian
+  ( vsucc U four Derived
+  ( vsucc U three Model
+  ( vsucc U two Spectra
+  ( vsucc U one T-Spectra
+  ( vsucc U zero Yogas
+  ( vzero U ))))))
+
+def Infinity : U := unit
+def Diagram : U := unit
+def LocalCartesianClosed : U := unit
+def SymmetricMonoidal : U := unit
+
+def nyid0 : Vec U four
+ := vsucc U three Infinity
+  ( vsucc U two Diagram
+  ( vsucc U one LocalCartesianClosed
+  ( vsucc U zero SymmetricMonoidal
+  ( vzero U ))))
+
+def к := summa (X: U), X
+
+def Being : Vec к ten
+ := vsucc к nine  (Vec U four, nyid0)
+  ( vsucc к eight (Vec U six,  nyid1)
+  ( vsucc к seven (Vec U five, nyid2)
+  ( vsucc к six   (Vec U zero, nyid3)
+  ( vsucc к five  (Sems,  star)
+  ( vsucc к four  (Body,  star)
+  ( vsucc к three (Mouth, star)
+  ( vsucc к two   (Nose,  star)
+  ( vsucc к one   (Ear,   star)
+  ( vsucc к zero  (Eye,   star)
+  ( vzero U ))))))))))