This commit is contained in:
Michael Zhang 2024-05-29 13:13:34 -05:00
parent 237248bdc2
commit ab8ba9f8bf
2 changed files with 31 additions and 9 deletions

View file

@ -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
```
_⋆
```

View file

@ -0,0 +1,9 @@
```
{-# OPTIONS #-}
module MayConcise.Chapter2 where
```
## 1 Categories
```
```