push

.editorconfig

@@ -0,0 +1,3 @@
+[*]
+indent_size = 2
+indent_style = space

.gitignore

@@ -1 +1,2 @@
 *.agdai
+.DS_Store

Makefile

@@ -1,7 +1,7 @@
 GENDIR := html/src/generated
 
 build-to-html:
-	find src/HottBook \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \
+	find src \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \
 	  | rust-parallel -0 agda \
 	  	--html \
 		--html-dir=$(GENDIR) \
@@ -17,6 +17,6 @@ refresh-book: build-to-html
 	mdbook serve html
 
 deploy: build-book
-	rsync -azrP html/book/ root@veil:/home/blogDeploy/public/hott-book
+	rsync -azrP html/book/ root@veil:/home/blogDeploy/public/research
 
 .PHONY: build-book build-to-html deploy

html/book.toml

@@ -13,12 +13,16 @@ macros = "./macros.txt"
 [preprocessor.chapter-zero]
 levels = [0]
 
+[preprocessor.graphviz]
+command = "mdbook-graphviz"
+output-to-file = false
+
 [output.html]
 additional-js = [
-    # "theme/pagetoc.js"
+  # "theme/pagetoc.js"
 ]
 additional-css = [
-    "Agda.css",
-    "style.css",
-    # "theme/pagetoc.css"
+  "Agda.css",
+  "style.css",
+  # "theme/pagetoc.css"
 ]

html/src/SUMMARY.md

@@ -1,6 +1,9 @@
 # Summary
 
 - [Front](./front.md)
+
+# HoTT Book
+
 - [Chapter 1](./generated/HottBook.Chapter1.md)
   - [Exercises](./generated/HottBook.Chapter1Exercises.md)
 - [Chapter 2](./generated/HottBook.Chapter2.md)
@@ -16,3 +19,6 @@
 - [Definition 3.3.1](./generated/HottBook.Chapter3Definition331.md)
 - [Lemma 3.3.3](./generated/HottBook.Chapter3Lemma333.md)
 
+# Van Doorn Dissertation
+
+- [Preliminaries](./generated/VanDoornDissertation.Preliminaries.md)

html/src/front.md

@@ -1,6 +1,24 @@
-# Homotopy Type Theory
+# Research
 
-I'm recreating a formalization for the Homotopy Type Theory book as I'm working through it to help me learn.
+This book tracks my current research goals and progress.
 
 - [Source](https://git.mzhang.io/school/type-theory)
 
+```dot process
+digraph {
+  rankdir="BT"
+
+  subgraph cluster_exploration {
+    label = "random cloud of exploration" {
+      mayconcise [label="concise course" URL="https://git.mzhang.io/school/type-theory/raw/branch/master/resources/MayConcise/ConciseRevised.pdf"]
+      hott [label = "hott book" URL="https://hott.github.io/book/hott-ebook.pdf.html"]
+    }
+  }
+
+  subgraph cluster_thesis {
+    label = "thesis" {
+      
+    }
+  }
+}
+```

html/src/hott-front.md

@@ -0,0 +1,3 @@
+# Homotopy Type Theory
+
+I'm recreating a formalization for the Homotopy Type Theory book as I'm working through it to help me learn.

resources/VanDoornDissertation/.gitignore

@@ -0,0 +1,3 @@
+*.aux
+*.log
+*.toc

resources/VanDoornDissertation/dissertation.tex

@@ -1,24 +1,41 @@
 \RequirePackage{fix-cm}
+\def\OPTpagesize{4.8in,7.9in}   % Page size
 \documentclass[12pt]{report}
 \usepackage[hyphens]{url}
-\usepackage{hyperref}
-\usepackage[margin=1.2in]{geometry}
-\pdfoutput=1
+\usepackage[
+  backref=page,
+  colorlinks,
+  citecolor=linkcolor,
+  linkcolor=linkcolor,
+  urlcolor=linkcolor,
+  unicode,
+]{hyperref}
+\usepackage[
+  papersize={\OPTpagesize},
+  margin=0.4in,
+  twoside,
+  includehead,
+]{geometry}
+% \pdfoutput=1
 \usepackage{lmodern}
 \usepackage[utf8x]{inputenc}
 \usepackage[T1]{fontenc}
-\usepackage{amsmath,mathtools,amssymb,etoolbox,enumerate,xspace}
+\usepackage{amsmath,amsfonts,mathtools,amssymb,etoolbox,enumerate,xspace}
 \usepackage{microtype}
+\usepackage{ctex}
 \usepackage{caption,subcaption}
 \mathtoolsset{mathic,centercolon}
 \usepackage[numbered]{bookmark}
 
+\def\OPTlinkcolor{0,0.45,0}   % RGB components for clickable links
+
 % footnotes numbered consecutively throughout chapters
 \usepackage{chngcntr}
 \counterwithout{footnote}{chapter}
 
 %% URL
 \usepackage{xcolor}
+\definecolor{linkcolor}{rgb}{\OPTlinkcolor}
 \usepackage{cleveref}
 \hypersetup{
   colorlinks,
@@ -45,6 +62,8 @@
 \protected\def\tikz@nonactivecolon{\ifmmode\mathrel{\mathop\ordinarycolon}\else:\fi} 
 \makeatother
 
+\linespread{1.05} % Palatino looks better with this
+
 
 
 %% Lean code
@@ -85,7 +104,7 @@
 %\renewcommand{\kappa}{\varkappa}
 % \renewcommand{\rho}{\varrho}
 \renewcommand{\phi}{\varphi}
-\renewcommand{\C}{\mathbb{C}}  
+\newcommand{\C}{\mathbb{C}}  
 
 \newcommand{\br}[1]{\langle#1\rangle}
 
@@ -172,7 +191,7 @@
 % \newcommand{\isprop}{\textnormal{is-prop}}
 % \newcommand{\prop}{\textnormal{Prop}}
 % \newcommand{\isset}{\textnormal{is-set}}
-\renewcommand{\U}{\UU}
+\newcommand{\U}{\UU}
 % \newcommand{\type}{\mathcal{U}}
 % \newcommand{\set}{\textnormal{set}}
 % \newcommand{\fa}[2]{\ensuremath{\Pi(#1),\ #2}}

src/MayConcise/Chapter1.lagda.md

@@ -0,0 +1,20 @@
+```
+{-# OPTIONS --cubical #-}
+module MayConcise.Chapter1 where
+```
+
+## 1 What is algebraic topology?
+
+https://en.wikipedia.org/wiki/Homomorphism
+
+> A homomorphism is a map between two algebraic structures of the same type (that is of the same name), that preserves the operations of the structures. This means a map f : A → B {\displaystyle f:A\to B} between two sets A {\displaystyle A}, B {\displaystyle B} equipped with the same structure such that, if ⋅ {\displaystyle \cdot } is an operation of the structure (supposed here, for simplification, to be a binary operation), then
+>
+> ```
+> f ( x ⋅ y ) = f ( x ) ⋅ f ( y ) {\displaystyle f(x\cdot y)=f(x)\cdot f(y)}
+> ```
+>
+> for every pair x {\displaystyle x}, y {\displaystyle y} of elements of A {\displaystyle A}.
+
+```
+homotopy : {X Y : Set} {p q : X → Y}
+```

src/VanDoornDissertation/HIT.lagda.md

@@ -0,0 +1,29 @@
+```
+{-# OPTIONS --cubical #-}
+module VanDoornDissertation.HIT where
+
+open import Data.Nat
+open import VanDoornDissertation.Preliminaries
+```
+
+# 3 Higher Inductive Types
+
+## 3.1 Propositional Truncation
+
+```
+data one-step-truncation (A : Set) : Set where
+  f : A → one-step-truncation A
+  e : (x y : A) → f x ≡ f y
+
+weakly-constant : {A B : Set} → (g : A → B) → Set
+weakly-constant {A} g = {x y : A} → g x ≡ g y
+
+definition3∙1∙1 : {A : Set} → one-step-truncation A → ℕ → Set
+definition3∙1∙1 {A} trunc zero = A
+definition3∙1∙1 {A} trunc (suc n) = one-step-truncation (definition3∙1∙1 trunc n)
+
+fs : {A : Set} → one-step-truncation A → (n : ℕ) → Set
+fs trunc n = (definition3∙1∙1 trunc n) → (definition3∙1∙1 trunc (suc n))
+
+-- lemma3∙1∙3 : {X : Set} → {x : X} → is
+```

src/VanDoornDissertation/Preliminaries.lagda.md

@@ -0,0 +1,89 @@
+```
+{-# OPTIONS --cubical #-}
+module VanDoornDissertation.Preliminaries where
+
+open import Agda.Primitive
+open import Agda.Primitive.Cubical
+```
+
+### 2.2.1 Paths
+
+```
+Path : {ℓ : Level} (A : Set ℓ) → A → A → Set ℓ
+Path A = PathP (λ i → A)
+
+infix 4 _≡_
+_≡_ : {ℓ : Level} {A : Set ℓ} → A → A → Set ℓ
+_≡_ {A = A} = Path A
+
+private
+  to-path : {ℓ : Level} {A : Set ℓ} → (f : I → A) → Path A (f i0) (f i1)
+  to-path f i = f i
+refl : {ℓ : Level} {A : Set ℓ} {x : A} → x ≡ x
+refl {x = x} = to-path (λ i → x)
+
+id : {l : Level} {A : Set l} → A → A
+id x = x
+
+ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A}
+  → (f : A → B)
+  → (p : x ≡ y)
+  → f x ≡ f y
+ap {l1} {l2} {A} {B} {x} {y} f p i = f (p i)
+  -- J (λ x y p → f x ≡ f y) (λ x → refl) x y p
+
+transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
+  → (P : A → Set l₂)
+  → (p : x ≡ y)
+  → P x → P y
+transport {l₁} {l₂} {A} {x} {y} P p = primTransp (λ i → P (p i)) i0
+```
+
+### 2.2.3 More on paths
+
+#### Pathovers
+
+```
+dependent-path : {A : Set} 
+  → (P : A → Set) 
+  → {x y : A} 
+  → (p : x ≡ y)
+  → (u : P x) → (v : P y) → Set
+dependent-path P p u v = transport P p u ≡ v
+
+syntax dependent-path P p u v = u ≡[ P , p ] v
+
+-- https://git.mzhang.io/school/type-theory/issues/16
+apd : ∀ {a b} {A : I → Set a} {B : (i : I) → A i → Set b}
+    → (f : (i : I) → (a : A i) → B i a)
+    → {x : A i0}
+    → {y : A i1}
+    → (p : PathP A x y)
+    → PathP (λ i → B i (p i)) (f i0 x) (f i1 y)
+apd f p i = f i (p i)
+```
+
+#### Squares
+
+```
+data square {A : Set} {a00 : A} : {a20 a02 a22 : A}
+    → a00 ≡ a20
+    → a02 ≡ a22
+    → a00 ≡ a02
+    → a20 ≡ a22
+    → Set
+  where
+  reflₛ : square refl refl refl refl
+```
+
+#### Squareovers and cubes
+
+```
+
+```
+
+#### Paths in type formers
+
+```
+
+```