concise course in algebraic topology

.gitattributes

@@ -0,0 +1 @@
+resources/* linguist-vendored

resources/MayConcise/lacromay.sty

@@ -0,0 +1,263 @@
+% LACROMAY.STY - Extra Math Definitions and Symbols
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{lacromay}[1998/07/22 v1.0
+ Extra Math Definitions and Symbols]
+%\RequirePackage{amssymb}[1995/01/01]
+%%   Change \lhd, \rhd to use the amssymb symbols
+\renewcommand{\lhd}{\vartriangleleft}
+\renewcommand{\rhd}{\vartriangleright}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\catcode`\ =9
+\endlinechar=-1 % Make things readable.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%   Setup to use Ralph Smith Formal Script font:
+\DeclareFontFamily{OMS}{rsfs}{\skewchar\font'60}
+\DeclareFontShape{OMS}{rsfs}{m}{n}{<-5>rsfs5 <5-7>rsfs7 <7->rsfs10 }{}
+\DeclareSymbolFont{rsfs}{OMS}{rsfs}{m}{n}
+\DeclareSymbolFontAlphabet{\scr}{rsfs}
+
+\let\overto\xrightarrow
+\def\circle{\mathaccent"7017}
+
+%Kate's macros
+\newcommand{\chara}{\operatorname{char}}
+\newcommand{\degree}{\operatorname{deg}}
+\newcommand{\Kernel}{\operatorname{Ker}}
+\newcommand{\image}{\operatorname{Im}}
+\newcommand{\Cokernel}{\operatorname{Coker}}
+
+% script letters  small s then capital letter
+\newcommand{\sA}{\scr{A}}
+\newcommand{\sB}{\scr{B}}
+\newcommand{\sC}{\scr{C}}
+\newcommand{\sD}{\scr{D}}
+\newcommand{\sE}{\scr{E}}
+\newcommand{\sF}{\scr{F}}
+\newcommand{\sG}{\scr{G}}
+\newcommand{\sH}{\scr{H}}
+\newcommand{\sI}{\scr{I}}
+\newcommand{\sJ}{\scr{J}}
+\newcommand{\sK}{\scr{K}}
+\newcommand{\sL}{\scr{L}}
+\newcommand{\sM}{\scr{M}}
+\newcommand{\sN}{\scr{N}}
+\newcommand{\sO}{\scr{O}}
+\newcommand{\sP}{\scr{P}}
+\newcommand{\sQ}{\scr{Q}}
+\newcommand{\sR}{\scr{R}}
+\newcommand{\sS}{\scr{S}}
+\newcommand{\sT}{\scr{T}}
+\newcommand{\sU}{\scr{U}}
+\newcommand{\sV}{\scr{V}}
+\newcommand{\sW}{\scr{W}}
+\newcommand{\sX}{\scr{X}}
+\newcommand{\sY}{\scr{Y}}
+\newcommand{\sZ}{\scr{Z}}
+
+% Font used for operads  small o then capital letter
+% in case I change my mind, give the font its own name
+\let\opsymbfont\mathcal
+
+\newcommand{\oA}{{\opsymbfont{A}}}
+\newcommand{\oB}{{\opsymbfont{B}}}
+\newcommand{\oC}{{\opsymbfont{C}}}
+\newcommand{\oD}{{\opsymbfont{D}}}
+\newcommand{\oE}{{\opsymbfont{E}}}
+\newcommand{\oF}{{\opsymbfont{F}}}
+\newcommand{\oG}{{\opsymbfont{G}}}
+\newcommand{\oH}{{\opsymbfont{H}}}
+\newcommand{\oI}{{\opsymbfont{I}}}
+\newcommand{\oJ}{{\opsymbfont{J}}}
+\newcommand{\oK}{{\opsymbfont{K}}}
+\newcommand{\oL}{{\opsymbfont{L}}}
+\newcommand{\oM}{{\opsymbfont{M}}}
+\newcommand{\oN}{{\opsymbfont{N}}}
+\newcommand{\oO}{{\opsymbfont{O}}}
+\newcommand{\oP}{{\opsymbfont{P}}}
+\newcommand{\oQ}{{\opsymbfont{Q}}}
+\newcommand{\oR}{{\opsymbfont{R}}}
+\newcommand{\oS}{{\opsymbfont{S}}}
+\newcommand{\oT}{{\opsymbfont{T}}}
+\newcommand{\oU}{{\opsymbfont{U}}}
+\newcommand{\oV}{{\opsymbfont{V}}}
+\newcommand{\oW}{{\opsymbfont{W}}}
+\newcommand{\oX}{{\opsymbfont{X}}}
+\newcommand{\oY}{{\opsymbfont{Y}}}
+\newcommand{\oZ}{{\opsymbfont{Z}}}
+
+\DeclareMathAlphabet{\eus}{U}{eus}{m}{n}
+%\SetMathAlphabet{\eus}{bold}{U}{eus}{b}{n}
+
+% Font used for categories  small a then capital letter
+%     would use small c but too many conflicts with xypic
+% in case I change my mind, give the font its own name
+\let\catsymbfont\eus
+
+\newcommand{\aA}{{\catsymbfont{A}}}
+\newcommand{\aB}{{\catsymbfont{B}}}
+\newcommand{\aC}{{\catsymbfont{C}}}
+\newcommand{\aD}{{\catsymbfont{D}}}
+\newcommand{\aE}{{\catsymbfont{E}}}
+\newcommand{\aF}{{\catsymbfont{F}}}
+\newcommand{\aG}{{\catsymbfont{G}}}
+\newcommand{\aH}{{\catsymbfont{H}}}
+\newcommand{\aI}{{\catsymbfont{I}}}
+\newcommand{\aJ}{{\catsymbfont{J}}}
+\newcommand{\aK}{{\catsymbfont{K}}}
+\newcommand{\aL}{{\catsymbfont{L}}}
+\newcommand{\aM}{{\catsymbfont{M}}}
+\newcommand{\aN}{{\catsymbfont{N}}}
+\newcommand{\aO}{{\catsymbfont{O}}}
+\newcommand{\aP}{{\catsymbfont{P}}}
+\newcommand{\aQ}{{\catsymbfont{Q}}}
+\newcommand{\aR}{{\catsymbfont{R}}}
+\newcommand{\aS}{{\catsymbfont{S}}}
+\newcommand{\aT}{{\catsymbfont{T}}}
+\newcommand{\aU}{{\catsymbfont{U}}}
+\newcommand{\aV}{{\catsymbfont{V}}}
+\newcommand{\aW}{{\catsymbfont{W}}}
+\newcommand{\aX}{{\catsymbfont{X}}}
+\newcommand{\aY}{{\catsymbfont{Y}}}
+\newcommand{\aZ}{{\catsymbfont{Z}}}
+
+% blackboard bold letters  b then capital letter
+%%   Change \Bbb to \mathbb (for consistency with other LaTeX2e math font
+%%   names):
+%\def\mathbb#1{\protect\text{$\protect\mathbb{#1}$}}
+
+% blackboard bold letters  b then capital letter
+%\def\mathbb#1{\protect\text{$\protect\Bbb{#1}$}}
+\newcommand{\bA}{\mathbb{A}}
+\newcommand{\bB}{\mathbb{B}}
+\newcommand{\bC}{\mathbb{C}}
+\newcommand{\bD}{\mathbb{D}}
+\newcommand{\bE}{\mathbb{E}}
+\newcommand{\bF}{\mathbb{F}}
+\newcommand{\bG}{\mathbb{G}}
+\newcommand{\bH}{\mathbb{H}}
+\newcommand{\bI}{\mathbb{I}}
+\newcommand{\bJ}{\mathbb{J}}
+\newcommand{\bK}{\mathbb{K}}
+\newcommand{\bL}{\mathbb{L}}
+\newcommand{\bM}{\mathbb{M}}
+\newcommand{\bN}{\mathbb{N}}
+\newcommand{\bO}{\mathbb{O}}
+\newcommand{\bP}{\mathbb{P}}
+\newcommand{\bQ}{\mathbb{Q}}
+\newcommand{\bR}{\mathbb{R}}
+\newcommand{\bS}{\mathbb{S}}
+\newcommand{\bT}{\mathbb{T}}
+\newcommand{\bU}{\mathbb{U}}
+\newcommand{\bV}{\mathbb{V}}
+\newcommand{\bW}{\mathbb{W}}
+\newcommand{\bX}{\mathbb{X}}
+\newcommand{\bY}{\mathbb{Y}}
+\newcommand{\bZ}{\mathbb{Z}}
+
+% Greek letters (first two letters, in small or cap; add z for variants)
+\newcommand{\al}{\alpha}
+\newcommand{\be}{\beta}
+\newcommand{\ga}{\gamma}
+\newcommand{\de}{\delta}
+\newcommand{\pa}{\partial}   %pretend its Greek
+%\newcommand{\ep}{\epsilon}
+\newcommand{\epz}{\varepsilon}
+\newcommand{\ph}{\phi}
+\newcommand{\phz}{\varphi}
+\newcommand{\et}{\eta}
+%\newcommand{\xi}{\xi}
+\newcommand{\io}{\iota}
+\newcommand{\ka}{\kappa}
+\newcommand{\la}{\lambda}
+%\newcommand{\mu}{\mu}
+%\newcommand{\nu}{\nu}
+\newcommand{\tha}{\theta}
+\newcommand{\thz}{\vartheta}
+%\newcommand{\pi}{\pi}
+\newcommand{\rh}{\rho}
+\newcommand{\si}{\sigma}
+\newcommand{\ta}{\tau}
+\newcommand{\ch}{\chi}
+\newcommand{\ps}{\psi}
+\newcommand{\ze}{\zeta}
+\newcommand{\om}{\omega}
+\newcommand{\GA}{\Gamma}
+\newcommand{\LA}{\Lambda}
+\newcommand{\DE}{\Delta}
+\newcommand{\SI}{\Sigma}
+\newcommand{\THA}{\Theta}
+\newcommand{\OM}{\Omega}
+\newcommand{\XI}{\Xi}
+\newcommand{\UP}{\Upsilon}
+\newcommand{\PI}{\Pi}
+\newcommand{\PS}{\Psi}
+\newcommand{\PH}{\Phi}
+
+% preserve old meaning of \ep when outside of math mode
+%\let\old@ep=\ep
+%\def\ep{\ifmmode\epsilon\else\old@ep\fi}
+% symbols --- three letter commands
+\newcommand{\com}{\circ}     % composition of functions
+\newcommand{\iso}{\cong}     % preferred isomorphism symbol
+\newcommand{\htp}{\simeq}    % homotopy symbol
+\newcommand{\ten}{\otimes}   % tensor product
+\newcommand{\add}{\oplus}    % direct sum
+\newcommand{\thp}{\ltimes}   % twisted half-smash product
+\newcommand{\sma}{\wedge}    % smash product
+\newcommand{\wed}{\vee}      % wedge sum
+
+\newcommand{\ef}{\text{$E_\infty\ $}}
+\newcommand{\af}{\text{$A_\infty\ $}}
+
+\newcommand{\ul}{\underline}
+
+%\gdef\overto#1{{\buildrel{#1}\over\longrightarrow}}
+\newcommand{\overfrom}[1]{\xleftarrow{#1}}
+
+\newcommand{\tand}{\text{\ \ and \ \ }}   %``and'' between formulas in display
+
+\newcommand{\ip}[1]{\text{$\left\langle#1\right\rangle$}} % inner product
+\newcommand{\rtarr}{\longrightarrow}
+\newcommand{\ltarr}{\longleftarrow}
+\newcommand{\from}{\longleftarrow}
+\newcommand{\monoto}{\lhook\joinrel\relbar\joinrel\rightarrow}
+\newcommand{\epito}{\relbar\joinrel\twoheadrightarrow}
+
+% operators
+\def\quickop#1{\expandafter\newcommand\csname #1\endcsname{\operatorname{#1}}}
+\quickop{Hom} \quickop{End} \quickop{Aut} \quickop{Tel} \quickop{Mic}
+\quickop{Ext} \quickop{Tor} \quickop{Id} \quickop{Coker} \quickop{Ker}
+\quickop{Lim} \quickop{Colim} \quickop{Holim} \quickop{Hocolim}
+\quickop{id} \quickop{tel} \quickop{mic} \quickop{coker}
+\quickop{colim} \quickop{holim} \quickop{hocolim} \quickop{im}
+
+% \limit --- lim sub right arrow
+\let\limit=\varinjlim
+% \colimit --- lim sub left arrow
+\let\colimit=\varprojlim
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% SETS - the macro \set and \sset
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% \sset, or ``singleton set'' denotes a set of the form \{ x \}.
+% An optional argument is the subscript.  This might typically used
+% for giving an indexing set.
+\newtoks\sset@tok
+\newcommand{\sset}[1]{\sset@tok={#1}\futurelet\sset@temp\sset@action}
+\def\sset@witharg[#1]{\text{$\left\{\the\sset@tok\right\}_{#1}$}}
+\def\sset@withoutarg{\text{$\left\{\the\sset@tok\right\}$}}
+\def\sset@action{\ifx\sset@temp[%]
+\let\sset@next=\sset@witharg\else\let\sset@next=\sset@withoutarg\fi\sset@next}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% End readability.
+\catcode`\ =10 \endlinechar=`\^^M
+\endinput % of macromay.sty
+
+
+
+
+
+

src/HottBook/Chapter2.lagda.md

@@ -738,31 +738,55 @@ open axiom2∙10∙3
 ### Theorem 2.11.1
 
 ```
--- theorem2∙11∙1 : {A B : Set}
---   → (eqv @ (f , f-eqv) : A ≃ B)
---   → (a a' : A)
---   → (a ≡ a') ≃ (f a ≡ f a')
--- theorem2∙11∙1 (f , f-eqv) a a' =
---   let
---     open ≡-Reasoning
---     mkQinv g α β = isequiv-to-qinv f-eqv
---     inv : (f a ≡ f a') → a ≡ a'
---     inv p = (sym (β a)) ∙ (ap g p) ∙ (β a')
---     backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
---     backward q = begin
---       ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a')  ⟩
---       ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
---       ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
---       id q ∎
---     forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
---     forward p = begin
---       (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩
---       (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {!   !} ⟩
---       (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {!   !} ⟩
---       id p ∎
---     eqv = mkQinv inv backward forward
---   in
---   ap f , qinv-to-isequiv eqv
+theorem2∙11∙1 : {A B : Set}
+  → (eqv @ (f , f-eqv) : A ≃ B)
+  → (a a' : A)
+  → (a ≡ a') ≃ (f a ≡ f a')
+theorem2∙11∙1 (f , f-eqv) a a' =
+  let
+    open ≡-Reasoning
+    mkQinv g α β = isequiv-to-qinv f-eqv
+    inv : (f a ≡ f a') → a ≡ a'
+    inv p = (sym (β a)) ∙ (ap g p) ∙ (β a')
+    backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
+    backward q = begin
+      ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a')  ⟩
+      ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
+      ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {!   !} ⟩
+      id q ∎
+    forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
+    forward p = begin
+      (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩
+      (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {!   !} ⟩
+      -- (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {!   !} ⟩
+      id p ∎
+    eqv = mkQinv inv backward forward
+  in
+  ap f , qinv-to-isequiv eqv
+```
+
+### Theorem 2.11.2
+
+```
+-- module theorem2∙11∙2 where
+--   i : {A : Set} {a x1 x2 : A}
+--     → (p : x1 ≡ x2)
+--     → (q : a ≡ x1)
+--     → transport (λ y → a ≡ y) p q ≡ q ∙ p
+--   i {A} {a} {x1} {x2} p q =
+--     J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1)
+--       (λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → {!  refl !}) a x3 q1)
+--       x1 x2 p q
+```
+
+### Theorem 2.11.3
+
+```
+theorem2∙11∙3 : {A B : Set} → {f g : A → B} → {a a' : A}
+  → (p : a ≡ a')
+  → (q : f a ≡ g a)
+  → transport (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ (ap g p)
+theorem2∙11∙3 p q = {!   !}
 ```
 
 ## 2.12 Coproducts

src/HottBook/Chapter6.lagda.md

@@ -3,6 +3,7 @@ module HottBook.Chapter6 where
 
 open import HottBook.Chapter1
 open import HottBook.Chapter2
+open import HottBook.Chapter2Lemma221
 ```
 
 # 6 Higher inductive types
@@ -10,12 +11,14 @@ open import HottBook.Chapter2
 ### Definition 6.2.2 (Dependent paths)
 
 ```
-dep-path : {A : Set} 
+definition6∙2∙2 : {A : Set} 
   → (P : A → Set) 
   → {x y : A} 
   → (p : x ≡ y)
   → (u : P x) → (v : P y) → Set
-dep-path P p u v = transport P p u ≡ v
+definition6∙2∙2 P p u v = transport P p u ≡ v
+
+syntax definition6∙2∙2 P p u v = u ≡[ P , p ] v
 ```
 
 Circle definition
@@ -27,28 +30,34 @@ postulate
   loop : base ≡ base
   S¹-elim : (P : S¹ → Set)
     → (p-base : P base)
-    → (p-loop : dep-path P loop p-base p-base)
+    → (p-loop : p-base ≡[ P , loop ] p-base)
     → (x : S¹) → P x
 ```
 
 ### Lemma 6.2.5
 
 ```
-lemma6∙2∙5 : {A : Set}
-  → (a : A)
-  → (p : a ≡ a)
-  → S¹ → A
+lemma6∙2∙5 : {A : Set} → (a : A) → (p : a ≡ a) → S¹ → A
 lemma6∙2∙5 {A} a p circ = S¹-elim P p-base p-loop circ
   where
     P : S¹ → Set
     P _ = A
 
+    p-base : P base
     p-base = a
 
-    p-loop : transport P loop a ≡ a
-    p-loop =
-      let wtf = lemma2∙3∙8 (λ x → {!   !}) loop in
-      {!    !}
+    p-loop : a ≡[ P , loop ] a
+    p-loop = transportconst A loop a ∙ p
+```
+
+### Lemma 6.2.8
+
+```
+lemma6∙2∙8 : {A : Set} {f g : S¹ → A}
+  → (p : f base ≡ g base)
+  → (q : (ap f loop) ≡[ (λ x → x ≡ x) , p ] (ap g loop))
+  → (x : S¹) → f x ≡ g x
+lemma6∙2∙8 {A} {f} {g} p q = S¹-elim (λ x → f x ≡ g x) p {!   !}
 ```
 
 ## 6.3 The interval