diff --git a/Lecture7.typ b/Lecture7.typ
new file mode 100644
index 0000000..a084265
--- /dev/null
+++ b/Lecture7.typ
@@ -0,0 +1,199 @@
+#import "prooftree.typ": *
+#import "@preview/showybox:2.0.1": showybox
+#import "@preview/commute:0.2.0": node, arr, commutative-diagram
+#import "@preview/cetz:0.2.2": *
+#set page(width: 5.6in, height: 9in, margin: 0.4in)
+
+#let isofhlevel = $sans("isofhlevel")$
+#let PathOver = $sans("PathOver")$
+#let ua = $sans("ua")$
+#let idtoeqv = $sans("idtoeqv")$
+#let Helix = $sans("Helix")$
+#let UU = $cal(U)$
+#let transport = $sans("transport")$
+#let base = $sans("base")$
+#let ap = $sans("ap")$
+#let loop = $sans("loop")$
+#let Circle = $bb(S)^1$
+#let idtoiso = $sans("idtoiso")$
+#let Nat = $sans("Nat")$
+#let Vect = $sans("Vect")$
+#let Bool = $sans("Bool")$
+#let carrier = $sans("carrier")$
+#let iseqclass = $sans("iseqclass")$
+#let isInjective = $sans("isInjective")$
+#let Type = $sans("Type")$
+#let reflexive = $sans("reflexive")$
+#let Even = $sans("Even")$
+#let isEven = $sans("isEven")$
+#let Prop = $sans("Prop")$
+#let isProp = $sans("isProp")$
+#let Set = $sans("Set")$
+#let isContr = $sans("isContr")$
+#let isIso = $sans("isIso")$
+#let isEquiv = $sans("isEquiv")$
+#let isSet = $sans("isSet")$
+#let zero = $sans("zero")$
+#let suc = $sans("suc")$
+#let Monoid = $sans("Monoid")$
+#let MonoidStr = $sans("MonoidStr")$
+#let MonoidAxioms = $sans("MonoidAxioms")$
+#let refl = $sans("refl")$
+#let defeq = $equiv$
+#let propeq = $=$
+
+= Synthetic Homotopy Theory
+
+We are talking about _the_ circle today!
+
+What do all these words mean?
+
+- #[
+  *Homotopy theory.* Study of topological spaces up to continuous deformation. You might have heard we don't distinguish coffee cup and donuts. But it's getting worse.
+
+  We don't distinguish bagels and rubber bands, even if the rubber band doesn't have any thickness. Topologists distinguish them, but we don't. If you cut a hole in a piece of paper, that's still a bagel.
+
+  They collapse many of the differences. The technical term is _continuous deformation_. As long as nothing is being torn apart, that's ok. (don't eat the bagel)
+]
+
+- #[
+  *Synthetic.* There's a coordinate system, and you can get the location of any objects in the system. You can just solve equations via algebra on the coordinate system instead. This is called the _analytic_ way of thinking. We are *not* doing that.
+
+  Instead, we are going back to the Euclidean geometry. "There's a line between two points" doesn't specify what the line actually is. This is called _synthetic_, since it's just based on the axioms.
+]
+
+=== Example
+
+The standard circle of size 1 is typically defined (_analytically_) as $ {(x, y) | x^2 + y^2 = 1} $
+
+We are not doing this. Instead, we are defining the circle as the combination of
+
+- a point $base$
+- some abstract $loop$ from $base$ to itself
+
+We don't necessarily know what it looks like, or know how it works. This is a _synthetic_ approach.
+
+#align(center)[#line(length: 4cm)]
+
+One question is: this picture looks reasonable, but how do we do this in type theory? The type theory doesn't provide a reasonable way to talk about the $loop$. But we can talk about paths in the type, so we can represent $loop$ as a path.
+
+=== Definition using Coq notation
+
+```
+Inductive Circle : U :=
+  | base : Circle
+  | loop : base ≡ base.
+```
+
+The $loop$ is a path constructor, which is not supported by Coq. How do we eliminate this circle (how do I define a function that uses a circle)?
+
+Mimicking the Coq notation again, we would have:
+
+```
+match (x : Circle) with
+| base => ...
+| loop => ...
+end
+```
+
+What should we do with the second case? This is already kind of suspicious since it doesn't have type $Circle$. Also, what should be the output obligation?
+
+Suppose we define a function $f : Circle -> A$. We probably want the $base$ point to be sent somewhere such that $f(base) : A$.
+
+Intuitively, there should also be a loop in $A$, that is a path, that is "$f(loop)$". The path should be $f(base) propeq f(base)$. We put quotes around "$f(loop)$" because $f(loop)$ doesn't actually type-check in the theory. What we need right now is the map on paths $ap_f (loop)$.
+
+=== Dependent cases
+
+If $A$ depends on the circle, we can take a fibrational view. Imagine there are many fibers over the circle on the ground. In this case, $f(base) : A(base)$. Then "$f(loop)$" is a line travelling through the collection of fibers that goes back to $base$. However, $ap_f (loop)$ doesn't travel through the fibers, which we need.
+
+How can we specify something that is crossing different fibers? Suppose there are a collection of fibers $B : A -> U$ and a path $p : x propeq_A y$. There are endpoints $b_x : B(x)$ and $b_y : B(y)$ that travels through the collection of fibers. There are several ways to define this.
+
+*Definition (path over).*
+
+$ PathOver(p, b_x, b_y) :defeq (transport^B (p, b_x) propeq b_y) $
+
+This is a path _in_ $B(y)$ between the transported $b_x$, which does the travelling between fibers.
+
+```
+match (x : Circle) with
+| base => (fb : B base)
+| loop => (... : PathOver loop fb fb)
+```
+
+=== Other examples of HITs
+
+List of things to ask ChatGPT:
+
++ Spheres in arbitrary dimensions (circle is dimension 1)
++ Suspension
++ Arbitrary dimension of truncation
++ Homotopy pushouts
+
+=== Algebraic topology
+
+Why the word "algebraic"? Algebraic means you want to find some algebraic _invariants_ under continuous deformation. "If I'm allowing myself to equate bagels and rubber bands, what are the essential properties that are still the same?" For example, the bagel has a hole, and the rubber band also has a hole in it. We can turn this into a number we can calculate.
+
+Why do we care about this property? How can we prove that a bagel is different from a solid ball? If you can prove that the number of holes is an invariant on the deformation process, then it's a good way to classify different objects.
+
+One important thing is called the *fundamental group*.
+
+=== Fundamental group
+
+Fundamental group only works when u have an element in the type. Suppose a space $X$ with a point $x_0 : X$. We can define a _group_ on the paths.
+
+$ { "paths" x_0 propeq x_0 } \/ "homotopy" $
+
+You can prove it satisfies all the group laws (refl, concatenation, inverse). We will reproduce this in type theory.
+
+#let trunc(x) = $bar.double #x bar.double$
+
+*Definition (fundamental group).* $ pi_1 (X, x_0) &:defeq trunc(x_0 propeq x_0)_0 \
+&:defeq trunc(Omega(X, x_0))_0 $
+
+We need the $x_0 propeq x_0$ to be a set, since it may have some higher structure.
+
+*Definition (loop space).* Loop space does not forget the interesting higher dimensional structures.
+
+$ Omega(X, x_0) :defeq (x_0 propeq x_0) $
+
+Now we can state the theorem.
+
+*Theorem.* $pi_1 (Circle, base) tilde.eq ZZ$.
+
+*Theorem.* $Omega(Circle, base) tilde.eq ZZ$.
+
+Quick proof sketch: expanding the definition, we are trying to prove: $base propeq base tilde.eq ZZ$.
+
+What do we need for equivalence? Function going right, function going left, and prove that there are inverses going both directions. Consider the easy case: $g : ZZ -> base propeq base$
+
+- $g(-1) = loop^(-1)$
+- $g(0) = refl$
+- $g(1) = loop$
+- $g(2) = loop dot loop$
+
+Intuitively, this represents "how many times are you going around the circle"? With the opposite direction being the negative numbers. There is a name for this, called *winding numbers*.
+
+The other direction $f : (p : base propeq base) -> ZZ$ is more complicated. We can't really do induction on the loop like the integers. The trick is to construct a *covering space*. In the case of the circle, this looks like a helix going up.
+The fiber of $base$ is $Z$. Then, you can follow the unknown path $p$ around the circle and simultaneously wind up and down the circular stairs.
+
+#image("winding.jpeg", height: 3in)
+
++ We want to build a helix.
++ Transport zero along the path $p$
++ The final number is the output, the *winding number*
+
+Define: $Helix : Circle -> UU$ (non-dependent case, so slightly easier)
+
+- $Helix(base) :defeq ZZ$
+
+We can define the result of the path $ZZ propeq ZZ$. But due to univalence, we can use an equivalence here instead.
+
+The successor function is a good equivalence to give us this winding functionality.
+
+- $Helix(loop) :defeq ua(suc) : ZZ propeq ZZ$
+
+Now, we can define $f$:
+
+$ f :defeq lambda p. transport^Helix (p, 0) $
+
+Then, prove that $f$ and $g$ are inverses of each other, and then you would prove that $base propeq base tilde.eq ZZ$.
\ No newline at end of file
diff --git a/winding.jpeg b/winding.jpeg
new file mode 100644
index 0000000..a7a4c18
Binary files /dev/null and b/winding.jpeg differ