library Rectification Campaign (#399)

* lexing imports without stepping on keywords * Library rectification: prelude. * Library rectification: data. * Library rectification: basics. * Library rectification: paths. * Library rectification: everything else? * unleash some more lexer Power Moves (@favonia) * stupid way to build all files (lol) * update README * update main README * wording * foo * fix my fix for comments * get rid of broken multiline comment support in imports * [vim] Disable syntax highlighting for import names. * some little formatting rampage * Highlight "public import".
RedPRL · Oct 16, 2018 · 8eff984 · 8eff984
1 parent d8b4c50
commit 8eff984
Show file tree

Hide file tree

Showing 58 changed files with 620 additions and 631 deletions.
diff --git a/README.md b/README.md
@@ -46,6 +46,10 @@ Features we intend to add in the near future:
 - algebraic effects and handlers for RedML
 
 
+## The `redtt` mathematical library
+
+See [library/README.md](library/README.md).
+
 
 ## Contributing Guidelines
 

diff --git a/library/J.red b/library/J.red
diff --git a/library/Makefile b/library/Makefile
@@ -2,7 +2,7 @@ OPAM=opam
 EXEC=${OPAM} config exec
 DUNE=${EXEC} dune --
 
-RED_FILES=$(wildcard *.red)
+RED_FILES=$(wildcard ./**/*.red)
 
 all:
 	for f in ${RED_FILES}; do echo $${f}; ${DUNE} exec -- redtt load-file $${f} || exit -1 ; done
diff --git a/library/README.md b/library/README.md
@@ -1,7 +1,7 @@
-redtt library
-=============
+redtt mathematical library
+==========================
 
-This directory contains various developments in redtt.
+This is the home of the `redtt` mathematical library.
 
 
 Style and conventions
@@ -14,3 +14,22 @@ We have no absolute rules, but try to adhere to the following:
 - Write multi-word semantic units with hyphen (`is-contr`, `weak-connection`)
 - Write subordinate semantic units with slash (`plus/assoc`, `symm/unit`)
 - Reserve `is-` and `has-` for h-propositions (`is-contr`, `has-hlevel`)
+
+Library structure
+-----------------
+
+- `prelude/` contains definitions that are expected to be needed in all `redtt`
+  developments.
+
+- `data/` contains the bare definitions of datatypes, and whatever functions can
+  be defined without needing other constructions and lemmas.
+
+- `basics/` contains basic theorems of cubical type theory, which might not be
+  needed everywhere.
+
+- `paths/` contains theorems about the higher dimensional structure of types in
+  cubical type theory, such as characterizations of loop spaces, etc.
+
+- `cool/` contains cool constructions and theorems which aren't needed by anything;
+  many new developments will first start in `cool/`, and become their own folders as
+  become more complex and mature.
diff --git a/library/hedberg.red → library/basics/hedberg.red b/library/hedberg.red → library/basics/hedberg.red
@@ -1,9 +1,6 @@
-import path
-import void
-import bool
-import or
-import connection
-import hlevel
+import prelude
+import data.void
+import data.or
 
 def stable (A : type) : type =
   neg (neg A) → A

diff --git a/library/isotoequiv.red → library/basics/isotoequiv.red b/library/isotoequiv.red → library/basics/isotoequiv.red
@@ -1,6 +1,4 @@
-import path
-import hlevel
-import equivalence
+import prelude
 
 -- yacctt: https://github.com/mortberg/yacctt/blob/master/examples/prelude.ytt#L374
 -- RedPRL: https://github.com/RedPRL/sml-redprl/blob/bd73932409ddc3479c8ded5ac32ae0d93d31874a/example/isotoequiv.prl

diff --git a/library/retract.red → library/basics/retract.red b/library/retract.red → library/basics/retract.red
@@ -1,12 +1,4 @@
-import path
-import connection
-import hlevel
-
-def is-section (A B : type) (f : A → B) : type =
-  (g : B → A) × (a : A) → path A (g (f a)) a
-
-def retract (A B : type) : type =
-  (f : A → B) × is-section A B f
+import prelude
 
 -- Adapted from https://github.com/HoTT/book/issues/718
 def path-retract/preserves-refl (A : type) (R : A → A → type)

diff --git a/library/complete-induction.red → library/cool/complete-induction.red b/library/complete-induction.red → library/cool/complete-induction.red
@@ -1,8 +1,8 @@
-import nat
-import path
-import unit
-import void
-import or
+import prelude
+import data.nat
+import data.unit
+import data.void
+import data.or
 
 def le : nat → nat → type =
   elim [

diff --git a/library/free-monoid.red → library/cool/free-monoid.red b/library/free-monoid.red → library/cool/free-monoid.red
@@ -1,4 +1,4 @@
-import list
+import data.list
 
 -- In this file, we try to relate the weak free monoid on a set (presented as a HIT) to the
 -- strict free monoid, presented as a list.

diff --git a/library/s1.red → library/cool/hopf.red b/library/s1.red → library/cool/hopf.red
@@ -1,12 +1,7 @@
-import path
-import connection
-import hlevel
-import equivalence
-import univalence
-
-data s1 where
-| base
-| loop (i : 𝕀) [∂[i] → base]
+import prelude
+import data.s1
+import data.s2
+import paths.equivalence
 
 def rotate/loop : (a : s1) → path _ a a =
   elim [
@@ -43,3 +38,13 @@ def rotate/equiv (a : s1) : equiv s1 s1 =
 
 def rotate/path (a : s1) : path^1 type s1 s1 =
   ua s1 s1 (rotate/equiv a)
+
+def hopf : s2 → type =
+  elim [
+  | base → s1
+  | surf i j →
+    comp 0 1 s1 [
+    | ∂[j] | i=0 → ua s1 s1 (id-equiv s1)
+    | i=1 → rotate/path (loop j)
+    ]
+  ]
diff --git a/library/invariance.red → library/cool/invariance.red b/library/invariance.red → library/cool/invariance.red
@@ -1,7 +1,5 @@
-import path
-import connection
-import equivalence
-import bool
+import prelude
+import data.bool
 
 -- This is ported from some RedPRL examples by Carlo Angiuli:
 -- https://github.com/RedPRL/sml-redprl/blob/master/example/invariance.prl
@@ -16,12 +14,11 @@ def fun→pair-is-equiv (A : type) : is-equiv^1 _ _ (fun→pair A) =
   λ p →
     ( (pair→fun A p, refl)
     , λ fib →
-      coe 1 0 (λ i → (pair→fun _ (fib.snd i), λ j → weak-connection/or _ (fib.snd) i j))
-      in λ j →
-        path
-          ((f : bool → A) × path (A × A) (f tt, f ff) p)
-          (shannon/path A (fib.fst) j, fib.snd)
-          (pair→fun A p, refl)
+      coe 1 0 (λ i → (pair→fun _ (fib.snd i), λ j → weak-connection/or _ (fib.snd) i j)) in λ j →
+      path
+        ((f : bool → A) × path (A × A) (f tt, f ff) p)
+        (shannon/path A (fib.fst) j, fib.snd)
+        (pair→fun A p, refl)
     )
 
 def fun→pair/equiv (A : type) : equiv (bool → A) (A × A) =
@@ -35,15 +32,12 @@ def swap-pair (A : type) (p : A × A) : A × A =
 
 def swap-fun (A : type) : (bool → A) → bool → A =
   coe 1 0 (swap-pair A) in λ i →
-    fun→pair/path A i → fun→pair/path A i
+  fun→pair/path A i → fun→pair/path A i
 
 def swap-fun/path (A : type) : (f : bool → A) → path _ (swap-fun A (swap-fun A f)) f =
   coe 1 0 (λ _ → refl) in λ i →
-    let swapcoe =
-      coe 1 i (swap-pair A) in λ j →
-        fun→pair/path A j → fun→pair/path A j
-    in
-    (f : fun→pair/path A i)
-    → path (fun→pair/path A i)
-        (swapcoe (swapcoe f))
-        f
+  let swapcoe =
+    coe 1 i (swap-pair A) in λ j →
+    fun→pair/path A j → fun→pair/path A j
+  in
+  (f : fun→pair/path A i) → path (fun→pair/path A i) (swapcoe (swapcoe f)) f
diff --git a/library/modal.red → library/cool/modal.red b/library/modal.red → library/cool/modal.red
@@ -1,5 +1,5 @@
-import path
-import bool
+import prelude
+import data.bool
 
 -- the core constructor (prev α M) is written using application notation in
 -- the surface language

diff --git a/library/moebius-boundary.red → library/cool/moebius-boundary.red b/library/moebius-boundary.red → library/cool/moebius-boundary.red
@@ -1,8 +1,7 @@
-import path
-import bool
-import s1
-import equivalence
-import isotoequiv
+import prelude
+import data.bool
+import data.s1
+import basics.isotoequiv
 
 def not/equiv : equiv bool bool =
   iso→equiv _ _ (not, (not, (not∘not/id/pt, not∘not/id/pt)))
@@ -30,8 +29,7 @@ def moebius-boundary→s1/commuting :
   elim [ tt → refl | ff → refl ]
 
 def moebius-boundary→s1/loop/filler (i j : 𝕀) (y : not/path i) : s1 =
-  let z : bool = coe i 1 y in not/path
-  in
+  let z : bool = coe i 1 y in not/path in
   comp 1 j (moebius-boundary→s1/loop-base i z) [
   | i=0 → moebius-boundary→s1/commuting y
   | i=1 → refl
@@ -49,8 +47,7 @@ def moebius-boundary→s1 (x : moebius-boundary) : s1 =
 def s1→moebius-boundary/base : moebius-boundary =
   (base, ff)
 
-def loop-path (b : bool) :
-  path moebius-boundary (base, b) (base, not b) =
+def loop-path (b : bool) : path moebius-boundary (base, b) (base, not b) =
   λ i → (loop i , `(vin i b (not b)))
 
 def s1→moebius-boundary/loop/filler (i j : 𝕀) : moebius-boundary =

diff --git a/library/patch-theory.red → library/cool/patch-theory.red b/library/patch-theory.red → library/cool/patch-theory.red
@@ -1,7 +1,8 @@
-import path
-import int
-import equivalence
-import univalence
+import prelude
+import data.int
+import paths.int
+import paths.equivalence
+import paths.sigma
 
 data patch where
 | num

diff --git a/library/path-retract.red → library/cool/path-retract.red b/library/path-retract.red → library/cool/path-retract.red
@@ -1,8 +1,6 @@
-import path
-import J
-import equivalence
-import isotoequiv
-import retract
+import prelude
+import basics.retract
+import basics.isotoequiv
 
 -- a retract of the path family is an equivalence
 

diff --git a/library/pointed.red → library/cool/pointed.red b/library/pointed.red → library/cool/pointed.red
@@ -1,7 +1,6 @@
-import path
-import bool
-import equivalence
-import isotoequiv
+import prelude
+import data.bool
+import basics.isotoequiv
 
 def ptype : type^1 = (A : type) × A
 

diff --git a/library/problem.red → library/cool/problem.red b/library/problem.red → library/cool/problem.red
@@ -1,12 +1,13 @@
-import path
-import pointed
-import nat
-import int
-import s1
-import omega1s1
-import s2
-import join
-import s3-to-join
+import prelude
+import data.s1
+import data.s2
+import data.s3
+import data.join
+import data.int
+import paths.s1
+import cool.s3-to-join
+import cool.pointed
+import cool.hopf
 
 -- from https://github.com/mortberg/cubicaltt/blob/pi4s3/examples/problem.ctt
 
@@ -40,5 +41,5 @@ def test0-4 : pΩ³ ps2 .fst = f4 test0-3
 def innerpath (i j : 𝕀) : s1 =
   coe 0 1 base in λ k → hopf (test0-4 i j k)
 
---let problem : path int (pos zero) (pos zero) =
+--def problem : path int (pos zero) (pos zero) =
 --  λ i → coe 0 1 (pos zero) in λ j → s1-univ-cover (innerpath i j)
diff --git a/library/quotient.red → library/cool/quotient.red b/library/quotient.red → library/cool/quotient.red
@@ -1,16 +1,7 @@
-import path
-import hlevel
-import truncation
-import equivalence
-import isotoequiv
-import retract
-
-data (A : type) (R : A → A → type) ⊢ quotient where
-| pt (a : A)
-| gl (a b : A) (p : R a b) (i : 𝕀) [
-  | i=0 → pt a
-  | i=1 → pt b
-  ]
+import prelude
+import data.truncation
+import data.quotient
+import basics.isotoequiv
 
 -- A "quotient" by a "0-coherent groupoid" is effective
 def quotient/effective

diff --git a/library/redml-examples.red → library/cool/redml-examples.red b/library/redml-examples.red → library/cool/redml-examples.red
@@ -1,4 +1,4 @@
-import bool
+import data.bool
 
 meta ⦉
 

diff --git a/library/s3-to-join.red → library/cool/s3-to-join.red b/library/s3-to-join.red → library/cool/s3-to-join.red
@@ -1,13 +1,9 @@
-import path
-import s1
-import s2
-import join
-import equivalence
-import isotoequiv
-
-data s3 where
-| base
-| cube (i j k : 𝕀) [∂[i j k] → base]
+import prelude
+import data.s1
+import data.s2
+import data.s3
+import data.join
+import basics.isotoequiv
 
 -- forward map
 

diff --git a/library/torus.red → library/cool/torus.red b/library/torus.red → library/cool/torus.red
@@ -1,20 +1,11 @@
-import path
-import s1
-import equivalence
-import isotoequiv
+import prelude
+import data.s1
+import data.torus
+import basics.isotoequiv
 
 -- cubicaltt version: https://github.com/mortberg/cubicaltt/blob/master/examples/torus.ctt
 -- cubical agda version: https://github.com/Saizan/cubical-demo/blob/hits-transp/examples/Cubical/Examples/Torus.agda
 
-data torus where
-| pt
-| p/one (i : 𝕀) [∂[i] → pt]
-| p/two (i : 𝕀) [∂[i] → pt]
-| square (i j : 𝕀)
-  [ ∂[i] → p/one j
-  | ∂[j] → p/two i
-  ]
-
 def t2c : torus → s1 × s1 =
   elim [
   | pt → (base, base)
@@ -53,7 +44,6 @@ def torus/s1s1/iso : iso (s1 × s1) torus =
   , c2t2c
   )
 
-
 def torus/s1s1/equiv : equiv (s1 × s1) torus =
   iso→equiv (s1 × s1) torus torus/s1s1/iso