There is a collaboration grant for a research group that I could apply for the master. But I think I will have enough with a suddenly first exposure to proof-based math courses, and I should study as much as possible to get good grades. It will be too much time to spend on both things. Maybe the next year I can think about it again

Well I did it but it was a very simple typechecker for expressions. I gave up when I tried to implement definitions

announcement (boosts appreciated)

We're delighted to announce the HoTTEST Summer School, which will take place online everywhere in the world during the months of July and August 2022.

The school will run both synchronously and asynchronously. The lectures will be delivered live (between 2:30-4pm UTC) and paired with various tutorial sessions run by teaching assistants. The course will also feature a discord-based all-hours Q&A and an online archive of all course materials so that participants can follow along on their own schedule.

This school is for everyone and anyone with some familiarity with abstract mathematics or theoretical computer science and an itching to learn about homotopy type theory. Our goal is to make homotopy type theory accessible to, and inclusive of, everyone who is interested, regardless of cultural background, age, ability, formal education, ethnicity, gender identity, or expression. We believe HoTT is for everyone, and are committed to fostering a kind, inclusive environment.

Read more: https://groups.google.com/g/homotopytypetheory/c/Ir2joc7imyI

Join the Discord: https://discord.gg/tkhJ9zCGs9

the proof

Prove that if $\sim$ is a relation on a set $S$, then the corresponding family $\mathscr P_\sim$ defined in 1.5 is indeed a partition of $S$: that is, its elements are nonempty, disjoint, and their union is $S$.

We will previously prove a lemma to use in the disjoint proof.

**Lemma 1**. $\forall a,b \in S (a \in [b]_\sim \implies [a]_\sim = [b]_\sim)$.

Proof: Suppose $a,b\in S$ and $a \in [b]_\sim$. To prove $[a]_\sim \subseteq [b]_\sim$., suppose an arbitrary $a' \in [a]_\sim$. We have $a' \sim a$ and $a \sim b$. Since $\sim$ is transitive, we have $a' \sim b$, therefore $a' \in [b]_\sim$. To prove $[b]_\sim \subseteq [a]_\sim$, suppose an arbitrary $b' \in [b]_\sim$. Then we have $b' \sim b$ and $a \sim b$. By symmetry, $b \sim a$, and by transitivity $b' \sim a$, therefore $b' \in [a]_\sim$. Therefore $[a]_\sim = [b]_\sim$, and by our assumptions the lemma is true. $\square$

**Proof of exercise 1.2**.

To prove that $\mathscr P_\sim$ is a partition of $S$, we need to prove that its elements are nonempty, disjoint, and their union is $S$.

(Non-empty) Suppose an equivalence class $A \in \mathscr P_\sim$. So there must be an $a \in S$ such that $A = [a]_\sim$. It can't be nonempty, since $\sim$ is reflexive so $a \in [a]_\sim$. Since $a$ was arbitrary, then no equivalence class is empty, hence the elements of $\mathscr P_\sim$ are nonempty.

(Disjoint) Suppose two equivalence classes $A, B \in \mathscr P_\sim$ such that $A \neq B$. Then we have $a, b \in S$ such that $A = [a]_\sim$ and $B= [b]_\sim$. Now suppose that it exists an element $x \in [a]_\sim \cap [b]_\sim$, therefore $x \in [a]_\sim$ and $x \in [b]_\sim$. By Lemma 1, we have $[a]_\sim = [x]_\sim = [b]_\sim$, but we assumed that $A \neq B$, so we get a contradiction. Therefore it doesnt exists any element in $[a]_\sim \cap [b]_\sim$.

(Union) Finally we will prove $\bigcup \mathscr P_\sim = S$.

($\subseteq$) Suppose an arbitrary element $x \in \bigcup \mathscr P_\sim$. Then it must exist a set $X \in \mathscr P_\sim$ such that $x \in X$. This must be its equivalence class $[x]_\sim \in \mathscr P_\sim$, which is indeed a subset of $S$.

($\supseteq$) Suppose an $x \in S$. We can construct the equivalence relation $[x]_\sim$, and it will be in $\mathscr P_\sim$. Since $x \in [x]_\sim$ and $[x]_\sim \in \mathscr P_\sim$ we have that $x \in \bigcup \mathscr P _\sim$.

We can finally conclude that $\mathscr P_\sim$ is a partition of $S$. $\square$

- main acc
- @Sugui@awoo.fai.st

Interested in logic, type theory, proof assistants and formal methods

Joined May 2022