hardcode version

Author: 5HT

CHANGELOG

@@ -4,9 +4,9 @@ Changelog
 14 APR 2022 Version 1.4.0 Microkernel Pipeline:
 
 * Microkernel Architecture: Kernel, Proof Shell, and Tactics Server with open binary protocols
-* NixOS package /applications/science/logic/anders/ [@suhr]
-* Homotopy Library Manual: https://anders.groupoid.space/library/
-* CNAME Alias HOMOTOPY DEV
+* NixOS package /applications/science/logic/anders/
+* Homotopy Library Manual: https://anders.groupoid.space/lib/
+* CNAME Alias HOMOTOPY.DEV
 
 27 JAN 2022 Version 1.1.1 Univalence:
 

LICENSE

@@ -1,6 +1,6 @@
 DHARMA License
 
-Copyright (c) 2016—2022 Groupoid Infinity
+Copyright (c) 2016—2025 Groupoid Infinity
 
 Permission to use, copy, modify, and/or distribute this software for any
 purpose with or without fee is hereby granted, provided that the above

README.md

@@ -138,22 +138,22 @@ Infinitesimal Modality was added for direct support of Synthetic Differential Ge
 Benchmarks
 ----------
 
-Intel i7-8700.
+Intel i5-12400.
 
 ```
 $ time dune build
 
-real    0m1.456s
-user    0m2.794s
-sys     0m0.564s
+real    0m0.985s
+user    0m1.917s
+sys     0m0.570s
 ```
 
 ```
-$ time dune exec anders check library/book.anders
+$ time dune exec anders check lib/book.anders
 
-real    0m0.468s
-user    0m0.051s
-sys     0m0.032s
+real    0m0.268s
+user    0m0.017s
+sys     0m0.017s
 ```
 
 # Anders: Homotopy Library

dune

@@ -12,6 +12,7 @@
                 lib/foundations/modal/infinitesimal.anders
                 lib/mathematics/algebra/algebra.anders
                 lib/mathematics/analysis/real.anders
+                lib/mathematics/analysis/topology.anders
                 lib/mathematics/categories/category.anders
                 lib/mathematics/categories/functor.anders
                 lib/mathematics/categories/abelian.anders

lib/mathematics/analysis/topology.anders

@@ -23,17 +23,18 @@ def isSetPi₁' (A: U₁) (B: A → U) (h: Π (x: A), isSet (B x)) : isSet₁ (
 
 def Ω := U → 𝟐
 def ℙ (X: U₁) := X → Ω
-def isSet-ℙ (X: U₁) : isSet₁ (ℙ X)
+
+def isSet-ℙ (X: U₁)
+  : isSet₁ (ℙ X)
  := isSetPi₁ X (λ (x: X), Ω) (λ (x: X), isSetPi₁' U (λ (_: U), 𝟐) (λ (_: U), boolset))
+
 axiom specify (X: U₁) : (X → Ω) → ℙ X
+
 def ∅ (X: U₁) : ℙ X := \ (_: X) (_: U), false
 def total (X: U₁) : ℙ X := \ (_: X) (_: U), true
 def ∈ (X: U₁) (el: X) (set: ℙ X) : U₁ := Path₁ (U → 𝟐) (set el) (\(_: U), true)
 def ∉ (X: U₁) (el: X) (set: ℙ X) : U₁ := Path₁ (U → 𝟐) (set el) (\(_: U), false)
 def ⊆ (X: U₁) (A B: ℙ X) := Π (x: X), (∈ X x A) × (∈ X x B)
-def ∁ (X: U₁) : ℙ X → ℙ X -- not (complement)
- := λ (h: ℙ X), λ (x: X) (Y: U), not (h x Y)
-def ∪ (X: U₁) : ℙ X → ℙ X → ℙ X -- or (union)
- := λ (h1: ℙ X) (h2: ℙ X), λ (x: X) (Y: U), or (h1 x Y) (h2 x Y)
-def ∩ (X: U₁) : ℙ X → ℙ X → ℙ X -- and (intersection)
- := λ (h1: ℙ X) (h2: ℙ X), λ (x: X) (Y: U), and (h1 x Y) (h2 x Y)
+def ∁ (X: U₁) : ℙ X → ℙ X := λ (h: ℙ X), λ (x: X) (Y: U), not (h x Y)
+def ∪ (X: U₁) : ℙ X → ℙ X → ℙ X := λ (h1: ℙ X) (h2: ℙ X), λ (x: X) (Y: U), or (h1 x Y) (h2 x Y)
+def ∩ (X: U₁) : ℙ X → ℙ X → ℙ X := λ (h1: ℙ X) (h2: ℙ X), λ (x: X) (Y: U), and (h1 x Y) (h2 x Y)

package.json

@@ -1,6 +1,6 @@
 {
   "name": "homotopy",
-  "version": "1.3.0",
+  "version": "1.4.0",
   "description": "Anders: Modal Homotopy Type System",
   "main": "",
   "scripts": {

src/frontend/anders.ml

@@ -10,7 +10,7 @@ type cmdline =
   | Indices | Girard | Silent | Irrelevance
 
 let help =
-"\nhttps://homotopy.dev/library/
+"\nhttps://homotopy.dev/lib/
 
   invocation = anders | anders list
         list = [] | command list

src/frontend/repl.ml

@@ -16,8 +16,7 @@ Information about command line options can be found at ‘anders help’."
 
 let banner =
   Printf.sprintf "Anders Proof Assistant version %Ld.%Ld.%Ld
-Copyright © 2021–2022 Groupoid Infinity."
-    Fuze.year Fuze.month Fuze.patch
+Copyright © 2021–2022 Groupoid Infinity." 1L 4L 0L
 
 let loaded : Files.t ref = ref Files.empty