It's easy to understand categories knowing Haskell and type theory

What should I learn before approaching homotopy type theory? Maybe category theory? Topology?

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

"every function is the composition of a surjection, followed by an isomorphism, followed by an injection" 🤔

Specifically, today I've learned the equivalence between monomorphisms and injections

I'm learning some category theory concepts in the algebra book I'm reading and it is very fun to learn!

Okay, it is an errata, this edition isn't the newest tho

I think there is an errata in this definition. It wouldn't be, $\exists a \in S$?

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

Two months ago I tried to do an implementation of the CoC in Haskell... I was very excited but I finally dropped it... I should continue it at some point

Sugui boosted

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.

Join the Discord: 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$

It took me 1-2 hours and I had to see some ideas from another textbook but I managed to do a somewhat complicated proof for me so I feel proud

I wonder how practical is to study a math textbook writing definitions and theorems in a proof assistant, and doing exercises in it. Mainly because of the divergence between set theory based definitions in the book and type theory definitions in the proof assistant

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.