From ab8ba9f8bf2b9967a44ac2a607fd18387fececcc Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 29 May 2024 13:13:34 -0500
Subject: [PATCH] update

---
 src/MayConcise/Chapter1.lagda.md | 31 ++++++++++++++++++++++---------
 src/MayConcise/Chapter2.lagda.md |  9 +++++++++
 2 files changed, 31 insertions(+), 9 deletions(-)
 create mode 100644 src/MayConcise/Chapter2.lagda.md

diff --git a/src/MayConcise/Chapter1.lagda.md b/src/MayConcise/Chapter1.lagda.md
index 0c6fc2e..085e298 100644
--- a/src/MayConcise/Chapter1.lagda.md
+++ b/src/MayConcise/Chapter1.lagda.md
@@ -1,20 +1,33 @@
 ```
-{-# OPTIONS --cubical #-}
+{-# OPTIONS #-}
 module MayConcise.Chapter1 where
+
+open import HottBook.Chapter1
 ```
 
 ## 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}.
+```
+```
+
+## 2 The fundamental group
 
 ```
-homotopy : {X Y : Set} {p q : X → Y}
+π₁ : (X : Set) → (x : X) → Set
+π₁ X x = x ≡ x
+```
+
+## 3 Dependence on the basepoint
+
+```
+γ : {X : Set} {x y : X} (a : x ≡ y) → π₁ X x ≡ π₁ X y
+γ a = {! a ∙ ?  !}
+```
+
+## 4 Homotopy invariance
+
+```
+_⋆ 
 ```
\ No newline at end of file
diff --git a/src/MayConcise/Chapter2.lagda.md b/src/MayConcise/Chapter2.lagda.md
new file mode 100644
index 0000000..9b6917a
--- /dev/null
+++ b/src/MayConcise/Chapter2.lagda.md
@@ -0,0 +1,9 @@
+```
+{-# OPTIONS #-}
+module MayConcise.Chapter2 where
+```
+
+## 1 Categories
+
+```
+```
\ No newline at end of file