Contact: | thanos@imd.ufrn.br (though you should use Zulip instead) |
HorĂĄrios de aula: | 24T56 [16h50â18h30] |
Sala: | A102 |
Monitoria/TA: | fmc.imd.ufrn.br |
Older semesters: | .. |
Info
Prereqs
- obvious:
- {will, time} to {pratice, study, research}
- required:
- some mathematical maturity: you should be able to reason and to express mathematical ideas in natural mathematical language;
- you must have learned well the main subjects of FMC1âdo contact me if you are unsure, especially given the weak (or inexistent) grading that frequently takes place in this course;
- familiarity with the general ideas and tools of abstract algebra;
- if you have not passed FMC2 yet, at the very least you must enroll in my FMC2 class this semester to take it in parallel with cats;
- if you want to revise some material related to FMC1 (IDMa, IRI, IDMb), do check the prereqs for my FMC2 class of this semester for useful information;
- if you want to revise some material related to FMC2, do check chapters 7â13 of fmcbook and maybe 2022.1âs site.
(Obs. 1:Â learn â pass.)
(Obs. 2: study â read.)
Syllabus
The principal objective of this «topics» course in category theory is to introduce categorial notions, tools, and vocabulary, with focus on connections and application in computer science. We should also be able to have primers in type theory and denotational semantics of programming languages; this will depend crucially on the interest and work of the students.
Categorias
Definitions and examples. Commutative diagrams. Definitions using arrows. Languages of functional programming as categories. Constructions in categories. Universal constructions. Epis and monos. Duality principle. Products and coproducts. Equalizers and coequalizers. Limits and colimits. Functors. Deduction systems as categories. Exponentials. CCC (Cartesian closed categories) and lambda calculus. Natural transformations. Yoneda lemma. Adjunction. Monads.
Bibliography
(Heard of libgen.rs?)
Main texts
- Awodey: Category Theory (2nd ed.)
- Barr & Wells: Category Theory for Computing Science (3rd ed.) (ctcs)
Auxiliar
- Goldblatt: Topoi
- Riehl: Category Theory in Context
- Leinster: Basic Category Theory
(Co)algebras and (co)induction
- Jacobs & Rutten: (Co)algebras and (Co)induction
Order theory
- Moschovakis: Notes on Set Theory (2nd ed.) (cap. 6)
- Davey & Priestley: Introduction to Lattices and Order [DP]
Boolean Algebras
- Halmos: Lectures on Boolean Algebras (1963)
- Bell & Machover: A course in Mathematical Logic (cap. 4)
Teoria dos tipos
Tips
- James Munkres: Comments on style
- Jean-Pierre Serre: How to write mathematics badly
- Don Knuth: Mathematical writing
- Paul Halmos: How to write mathematics
Tecnologias e ferramentas
Obs.: As tecnologĂas/ferramentas seguintes podem mudar durante a disciplinaâexceto a primeira.
- PAPEL (um caderno para dedicar Ă disciplina) e LAPIS/CANETA.
- Zulip (leia o FAQ).
Regras
- Nunca escreva algo que vocĂȘ mesmo nĂŁo sabe explicar: (i) o que significa; (ii) seu papel na tua resolução. Por exemplo: um aluno escreveu a frase seguinte na sua demonstração: «Como f Ă© cancelĂĄvel pela esquerda temos que g=h». Ele deve saber o que significa ser cancelĂĄvel pela esquerda e tambĂ©m explicar como isso foi usado e/ou o que isso tem a ver com essa parte da sua demonstração.
- Qualquer trabalho poderå ser questionado em forma de prova oral, em modo privado ou aberto. Se um aluno não consegue explicar o que ele mesmo escreveu numa resolução, serå considerado plågio (veja abaixo).
- Participando, nunca dĂȘ uma resposta que tu nĂŁo pensou sozinho, exceto dando os crĂ©ditos correspodentes.
- NĂŁo tente âforçar a barraâ perguntando ou respondendo coisas aleatĂłrias com objetivo Ășnico de ganhar pontos. Os pontos de participação nĂŁo correspondem em apenas perguntas ou dĂșvidas que mostram interesse. O interesse Ă© implĂcito pelo fato que tu escolheu matricular nesta turmaânĂŁo vale pontos.
- NĂŁo procurem informaçÔes ou resoluçÔes em qualquer lugar fora dos indicados em cada homework. O Ășnico recurso aceitĂĄvel para procurar ajuda Ă© no nosso Zulip (especificamente seus canĂĄis pĂșblicosânĂŁo DM) e a monitoria.
- Proibido consultar o apĂȘndice de resoluçÔes do fmcbook durante a disciplina exceto quando for explicitamente permitido por mim. (Os apĂȘndices de dicas sĂŁo permitidos sim.)
Uns deveres dos alunos
- Visitar o site e o Zulip da disciplina pelo menos uma vez por dia durante o semestre. (Qualquer coisa postada no site ou no Zulip da disciplina serĂĄ considerada como conhecida por todos os alunos da turma.)
- Estudar o conteĂșdo lecionado e tentar resolver todos os trabalhos atribuidos.
- Participar no Zulip diariamente, compartilhando tuas resoluçÔes para receber feedback, e checando as resoluçÔes de outros colegas para dar feedback.
- Checar e atender seu email cadastrado no SIGAA pelo menos uma vez por dia durante o semestre.
- Participar nas aulas! Obs.: tendo uma dĂșvida durante a aula, levante a mĂŁo para solicitar âa falaâ e assim que a receber, pergunte! NĂŁo espere o fim da aula para discutir tua dĂșvida em âmodo particularâ! A maioria das vezes eu vou negar isso e pedir ao aluno iniciar a discussĂŁo no Zulip ou na prĂłxima aula.
- Participar nas aulas de exercĂcios de monitoria e utilizar seus horĂĄrios de tirar dĂșvidas.
(Veja também os FAQs relevantes.)
Sobre plĂĄgio
- PlĂĄgio detectado implica que o aluno serĂĄ reprovado imediatamente por nota e por faltas.
- Entregar tuas resoluçÔes para um aluno copiar é proibido do mesmo jeito, e também não ajuda mesmo ninguém.
Cadernos vs. celulares
NĂŁo faz sentido aparecer na aula sem caderno. E nĂŁo faz sentido aparecer na aula com celular ligado; bote no modo aviĂŁo antes de entrar na sala. As aulas sĂŁo interativas e se nĂŁo pretende participar e concentrar nesses 100 minutos, sugiro ficar fora e escolher uma outra maneira de passar teu tempo. NĂŁo Ă© necessĂĄrio (e obviamente nem suficiente) aparecer nas minhas aulas para passar.
Avaliação e faltas
Disclaimer. Eu suponho que os alunos desta turma escolheram se matricular por interesse em aprender seu conteĂșdo. O ideal seria ignorar assuntos irrelevantes de avaliação, presenças, carga horĂĄria, etc., e se jogar nos estudos.
Avaliação
A nota final de cada aluno vai ser principalmente baseada em um ou mais dos: (i) provas escritas; (ii) sua participação; (iii) trabalhos atribuidos; (iv) hw resolvidos (veja o FAQ relevante).
Cada aluno serĂĄ responsĂĄvel para manter organizado e bem escrito o seu caderno com todos os teoremas e exercĂcios que estudou durante a disciplina.
Presenças e faltas
A presença pela regulação da UFRN é obrigatória. Os alunos que não gostam/querem/podem aparecer nas minhas aulas ainda tem chances de ganhar até nota måxima e aprovar na disciplina. Ou seja: alunos que escolhem não participar ou aparecer nas aulas, e mesmo assim aparecem nas provas escritas e conseguem nota final de aprovação vão ter sua porcentagem de faltas ajustada para não reprovar por faltas. Esclarecimento: alunos que não conseguem nota final de aprovação não terão sua porcentagem de presença ajustada de jeito nenhum e por nenhum motivo.
Obviamente, alunos que nĂŁo aparecem nas aula nĂŁo terĂŁo como ganhar pontos de participaçãoâduh!ânem acesso nos pontos de possĂveis provas-surpresas.
As presenças/faltas serão cadastradas usando o sistema Plickers (veja o FAQ relevante).
Atrasados
Definição (atrasado). Seja $a$ aluno desta turma. Dizemos que $a$ é atrasado sse $a$ não estå jå sentado na sua mesa, com seu caderno jå aberto, seu celular jå desligado e na mochila, no momento que a aula começa.
Tentem estar presentes na sala da aula ANTES do horårio do seu começo, e fiquem até o fim da aula.
Caso que alguĂ©m chega atrasado: nĂŁo faz sentido bater na porta da sala de aula; nĂŁo faz sentido cumprimentar nem o professor (nĂŁo Ă© mostra educação cumprimentar nesse casoâpelo contrĂĄrio!) nem os amigos/colegas da aula. Entrando numa sala onde a aula jĂĄ começou, tentem fazer sua entrada o menos possĂvel notada por os participantes pois atrapalha a concentração de todos.
FAQs
Dynamic content
Scoreboard
Exams
Categories
- Prova 1.1 (2023-04-12) { uncensored , correçÔes }
Orders
- Prova 1.2 (2023-05-15) { uncensored , correçÔes }
Homework
Leia bem o FAQ sobre hw. Note também que:
- Homeworks are also assigned during classes and on Zulip.
Inventory of cats đ
- đ, đ, đ, đ, âŠ
- $\mathbf{Set}$, $\mathbf{Set_{\mathsf{fin}}}$, $\mathbf{Set_{\mathsf{inj}}}$
- $\mathbf{Set_{\star}}$
- $\mathbf{Semigroup}$, $\mathbf{Monoid}$, $\mathbf{Group}$, $\mathbf{Abel}$, $\mathbf{Ring}$
- $\mathbf{Poset}$
- â(S), where S is a set (discrete categories)
- â(âł), where âł is a monoid
- â(đą), where đą is a group
- â(đ«), where đ« is a proset
- $\mathbf{Int}_{(\mid)}$
- $\mathbf{Int}_{(\leq)}$
- $\mathbf{Set}_{(\subseteq)}$
- â(L), where L is a typed programming language
- â(D), where D is a logic derivation system
2023-03-14: (hw1._)
- Verify that the alleged examples of categories we saw in class, are indeed categories.
- Can we prove uniqueness for initial objects?
- What about terminal ones? [Give a nice answer on this one.]
- Drawâno looking!âdiagrams whose commutativity means:
- the identities laws
- the associativity law
- that a function Ï : A â B respects a binary operation on A
- that a function Ï : A â B respects a unary operation on A
- that a function Ï : A â B respects a constant of A
- that a binary operation on A is commutative
- In the diagram with two adjacent squares we saw in class, prove that if both squares commute, the whole diagram commutes.
- Let â be a category with only one object â. What can you tell about the collection â(â,â)?
- Consider đ having natural numbers as objects and let đ(n,m) be the collection of all matrices of size nĂm. Complete this idea to create an actual category.
- Let $\mathbf{Pos}$ have as objects all posets. Which should be the arrows here?
- Let $L$ be a typed programming language. To make a category out of $L$, consider its types as objects. What should the arrows be? What features must this language have in order for this to work out?
- Let $S$ be a set. How can we turn this as a category?
- Let $P$ be a pointed set. How can we turn this as a category?
2023-03-27: (hw2._)
- We saw one way to turn a pointed set into a category. Give another one.
- Show that in the definition of isomorphism, we cannot infer the commutativity of one part of the diagram, given the other.
- Is the inverse of an arrow unique?
- Show that (â ) is an equivalence relation.
- Write (by yourself) the definition of product in a category.
- Find to what concept «initial» and «terminal» translate within each of the categories we have met so far.
- In particular, do this for $\mathbf{Ring}$.
- Do the same for the concept of «product».
- Dualize the definition of a product to define the coproduct.
- Observe that dualizing twice yields the original definition, and therefore get the joke that «for a category theorist, every nut is a coconut» đ„„.
- Find to what concept «coproduct» translates within each of the categories we have met so far.
- Prove âuniquenessâ for: terminal objects, initial objects. (Why the quotation marks?)
- Prove âuniquenessâ for: products, coproducts.
- In class we defined monoid and group from the point of view of category theory. Do the same for groupoid.
- Knowing already about groups, rings, etc., we have defined the category $\mathbf{Group}$ of groups, the category $\mathbf{Ring}$ of rings, etc. But now we also know what a category is. (How) would you define the category $\mathbf{Cat}$ of categories?
2023-03-31
- ctcs, §§2.1â2.5
2023-04-03: (hw3._)
- Verify that †is initial in $\mathbf{Ring}$.
- Is there a terminal in $\mathbf{Ring}$?
- $\langle \mathit{outl}, \mathit{outr} \rangle = 1_{A\times B}$
- $\langle f \circ h, g \circ h \rangle = ?$
- $1_A \times 1_B = ?$
- $(\times)$-assoc
- $(\times)$-com
- Is 1 an identity for $(\times)$?
- Is 0 an identity for $(+)$?
- Is 0 an annihilator for $(\times)$?
- $(f \times h) \circ \langle g,k \rangle = ?$
- $(f \times h) \circ (g \times k) = ?$
- f Ă g â ?
- f + g â ?
- Prove that within $\mathbf{Group}$ the not-so-white lies mathematicians tend to say and believe do not lead to confusions:
- mono means inj homo
- epi means surj homo
- iso means mono & epi
- iso means bij homo
- Find counterexamplesâobviously not in $\mathbf{Group}$âfor each of these misconceptions.
- as a particular hint: verify that in $\mathbf{Monoid}$, the canonical âinclusionâ ââȘ†is epic but not surjective.
- In $\mathbf{Set}$, prove:
- inj â mono?
- inj â mono?
- surj â epi?
- surj â epi?
- mono â split mono?
- mono â split mono?
- epi â split epi?
- epi â split epi?
- We discussed some equations about pairing
âš_,_â©
and the product of arrows_Ă_
. Infer (and establish) the corresponding equations about copairing $\left\{{{\vphantom f-} \atop {\vphantom g-}}\right\}$ and the coproduct of arrows_+_
(aka_âšż_
).
2023-04-04
- ctcs, §§2.7
2023-04-05 (hw4._)
- $(\mathbb C\downarrow C)^{\mathrm{op}} = {?} $
- $(\mathbb C\uparrow C)^{\mathrm{op}} = {?} $
- $(\mathbb C^{\to})^{\mathrm{op}} = {?} $
- Which of the following are functors?
- $(\mathbb C / {-}) : \mathbf{Cat} \to \mathbf{Cat}$
- $({-} / \mathbb C) : \mathbf{Cat} \to \mathbf{Cat}$
- $({-})^{\mathrm{op}} : \mathbf{Cat} \to \mathbf{Cat}$
- $({-})^{\to} : \mathbf{Cat} \to \mathbf{Cat}$
- Find a functor from $\mathbf{Set}$ to $\mathbf{Group}$
2023-04-10 (hw5._)
- Define coequalizers
- Figure out to what known concept coequalizers correspond to, in đđđ
- Prove that equalizers are mono
- Investigate the converse
- Prove that epic equalizers are iso
- Does đđđ have an initial object?
- Does đđđ have finite products?
- (How) can we define â+đ»?
2023-04-18 (hw6._)
- Investigate $\mathrm{Hom}({-},B)$
- T.f.a.e:
- (i) $f : X \to Y$ iso in â
- (ii) $(\forall C\in\mathbb C)[ \text{$(f \circ) \equiv f_* : \mathbb{C}(C,X) \to \mathbb{C}(C,Y)$ bijective} ]$
- (iii) $(\forall C\in\mathbb C)[ \text{$(\circ f) \equiv f^* : \mathbb{C}(Y,C) \to \mathbb{C}(X,C)$ bijective} ]$
- in any proset, (â ) is an equivalence relation
- joins and meets are determined up to (â )
- How would you define $(<)$ in a proset?
2023-04-24 (hw7._)
- We defined two candidate-p(r)osets for PĂQ. Can you pick one?
- We defined two candidate-p(r)osets for P+Q. Can you pick one?
- [DP]: Exercises: 1.1, 1.2, 1.3, 1.7, 1.8, 1.9, 1.10, 1.27
2023-04-24 (hw8._)
- Prove:
- đȘ(Pâ1) â đȘ(P)â1
- đȘ(1âP) â 1âđȘ(P)
- đȘ(PâQ) â đȘ(P)ĂđȘ(Q)
- [DP]: Exercises: 1.5, 1.11, 1.12, 1.13, 1.18, 1.19, 1.22, 1.23, 1.24, 1.26
2023-05-04 (hw9._)
- Can you find a non-distributive lattice?
- Which of the P(r)oset constructions/operations we have defined work for lattices? (Donât forget the vertical sum $(\overline{\oplus})$ of Exercise 1.18.)
- [DP]: Exercises: 1.27
- [DP]: Exercises: 2.1, 2.2, 2.5, 2.6, 2.10, 2.11
2023-05-09 (hw10._)
- Can you find a non-modular lattice?
- Prove (safe-distr)
- Prove (safe-modul)
- Rewrite the proof of our first fixpoint theorem (no peeking!)
2023-05-10 (hw11._)
- Q: Is there a lattice that has no infinite chain, but has finite length?
- Find a lower-adjoint for the function (3·_) : †â â.
- Î. A proset that has all meets, also has all joins
- Are (binary) meets guaranteed in (AâB)?
- Î. Distributive lattice â Modular lattice
- Î. T.f.a.e.:
- (i)
(âaâ„c)[ aâ§(bâšc) = (aâ§b)âšc ]
- (ii)
(âaâ„c)[ aâ§(bâšc) = (aâ§b)âš(aâ§c) ]
- (i)
- Consider the following proposition:
- (â) if neither of (âšt) and (â§t) distinguishes u and v, then u = v
- (i) Understand what (â) means and spell it out in a proposition
- (ii) Prove (â) for distributive lattices
- (iii) Find witnesses for its failure in đâ and in đâ
- (iv) Conclude: distributive â (â)
- Prove the đââđâ theorem
- Î. Let P be an inhabited poset. T.f.a.e.:
- (i) P is a complete lattice
- (ii) âS exists for all SâP
- (iii) P has †and âS exists for all inhabited SâP
- Î. Let L, K be lattices, and f : L â K a map. T.f.a.e.:
- (i) f order-preserving
- (ii) f âpostponesâ joins:
f(aâšb) â„ fa âš fb
- (iii) f âpreponesâ meets:
f(aâ§b) †fa ⧠fb
- [DP] 2.25, 2.26, 2.35, 4.3, 4.6
2023-05-19 (hw12._)
- How would you define the free lattice $\mathcal L(A)$ generated by some set of generators $A$?
- The free monoid $\mathcal M(A)$?
- The free group $\mathcal G(A)$?
- Draw the free lattice generated by $b \leq a$ and $c$.
2023-05-23 (hw13._)
- Prove that what we claimed to be the free monoid âł(A), really is.
- What is the coproduct of bottomed (also called pointed) posets?
- What is the product of groups? What about abelian groups?
- What is the coproduct of abelian groups? What about groups?
2023-05-25 (hw14._)
- Prove that in đđđđ„, GĂH is a coproduct of G,H.
- In đđ«đšđźđ©, find commutative groups G,H, such that GĂH is not the coproduct of G,H.
- Let D be a discrete poset. Then: D cc â D = {â} â D flat.
- Which of the following are cc?:
- $(\wp A ; \subseteq)$
- $((A\rightharpoonup B);\sqsubseteq)$
- $((A\stackrel{\textrm{\tiny inj~}}{\rightharpoonup} B);\sqsubseteq)$
- (Chains(P);â)
- Ï
- Ï+1
- á
- $A^{<\omega}$
- $A^{\leq\omega} (= A^{<\omega} \cup A^{\omega})$
2023-05-29 (hw15._)
- Î. Let P,Q be cc posets and Ï : P â Q monotone. Then: Ï is countably continuous iff for every non-decreasing sequence xâ †xâ †⯠in P, Ï(limâxâ) = limâ (Ï xâ)
- Prove the «strongly least» part of the fixpoint theorem.
- Show easily that $\pi = \lambda f\,.\,\lambda n\,.\,\sum_{i=0}^n (f\, i)$ is continuous mapping of ((âââ)â(âââ)) and compute:
- $\pi\,\mathit{double}\; 2$
- $\pi\,(\lambda n\,.\,n^2 + 1)\; 3$
- $\pi^2\,\mathit{double}\; 2$
2023-06-02
- [awodey], cap 3: «Duality»
- ctcs, §§2.6â2.9
2023-06-09: Boolean algebras (BA._)
- Can we have criteria similar to the one-test of groups for boolean homomorphisms?
- In a finite lattice, each filter $F$ is principal (i.e., generated by a single element $F = (x \leq {})$.
- If $A$ has the fipâą (or «$A$ fips») then $A \cup \{x\}$ fips or $A \cup \{xâ\}$ fips.
(Better term: «fmp», for «finite meet property». Definition: $A$ has the fmp iff finite meets from A are non-zero:
(âaâ,âŠ,aâ)[ aââ§âŻâ§aâ â 0 ]
.) - Let $(A_i)_{i\in I}$ be a chain of subsets of $B$ that fip. Show that $\bigcup_i A_i$ fips.
- Let $\underline A$ be the set of all infima of all finite subsets of $A$.
A base for a filter $F$ is a set $A$ such that $A^{\uparrow} = F$.
A subbase for a filter $F$ is a set $A$ such that $\underline A$ is a base for $F$, so that $F = {(\underline A)}^{\uparrow}$.
We say that $A$ generates $F$. Note that $A \subseteq \underline A \subseteq (\underline A)^{\uparrow}$.
Let $A$ be a subset of a boolean algebra $B$.
Prove the following:
- The set $(\underline A)^{\uparrow}$ is a filter.
- Any filter containing $A$ contains $(\underline A)^{\uparrow}$.
- $(\underline A)^{\uparrow}$ is proper iff $A$ fips.
- Let $F$ be a filter for a boolean algebra $B$. $F$ is an ultrafilter iff for each $b\in B$, either $x \in F$ or $xâ \in F$ but not both.
- Show that $X$ is a filter iff $Xâ = \{xâ \mid x \in X\}$ is an ideal.
- Let $B$ be a boolean algebra, and let $F$ be a filter in $B$. Show that $\hat B = F \cup Fâ \leq B$ and $F$ is an ultrafilter in $\hat B.$
- Let $\varphi : B \to C$ be a homomorphism of boolean algebras. Show that $\varphi$ is injective iff its kernel $\varphi^{-1}(0)$ is a singleton iff its hull $\varphi^{-1}(1)$ is a singleton.
- (From homos to filters:) Let f : BâC be a homomorphism and let H be its hull. H is a filter.
- (From filters to homos:) Let F be a filter of B.
Define the operations $(\rightarrow),(\leftrightarrow)$ on $B$ by:
$x \mathbin{\rightarrow} y = (xâ \vee y)$;
$x \mathbin{\leftrightarrow} y = (x \mathbin{\rightarrow} y) \wedge (y \mathbin{\rightarrow} x)$.
Define the relation $(\sim_F)$ on $B$ by: $$x \sim_F y \iff (x \liff y) \in F.$$
- Prove that $(\sim_F)$ is an equivalence relation.
- Prove that $(\sim_F)$ is a congruence for $B$.
- The above means that the set B/F of $(\sim_F)$-classes can be turned into a boolean algebra in the usual way. Prove that the standar projection $h : B \to B/F$ defined by $h(x) = [x]_{\sim_F}$ is a homomorphism from $B$ onto $B/F$, $F$ is the hull of $h$, where hull(h) = hâ»Âč(1).
- Let h : B â Bâ be a homomorphism of Boolean algebras and let Fâ be the hull of h. Show that the image h[B] â B/Fâ.
- The following conditions on a filter F in a boolean algebra B are equivalent:
- (a) B/F â đ;
- (b) F is the hull of a đ-valued homomorphism h : B â đ;
- (c) F is an ultrafilter;
- (d) F is prime;
- (e) for any b â B, either b or bâ is in F.
- Prove the Ultrafilter Theorem: Every filter in a boolean algebra can be extended to an ultrafilter.
âŠor at least prove the following corollaries:
- Each set of elements of a boolean algebra having the fip can be extended to an ultrafilter.
- Each non-zero element of a boolean algebra is contained in some ultrafilter.
- If xâ y then there is an ultrafilter containing one but not the other.
2023-06-15 (hw16._)
- Prove what we didnât in class: the lfp(Ï) for the factorial is a total function.
- Give polynomial functors T that correspond to T-algebras adequate to describe algebraic structures and inductive data types that you care about.
- Understand the statement that [O,S] : 1 + â â â is a (1 + _)-algebra on â.
- Define the following functions to streams:
map : (a â b) â Stream a â Stream b
zip : (Stream a, Stream b) â Stream (a,b)
only : a â Stream a
upFrom : Nat â Stream Nat
downFrom : Nat â Stream Nat
loop : Nat â Stream a â Stream a
merge2 : (Stream a, Stream a) â Stream a
preConcat : Nat â Stream a â Stream a â Stream a
drop : Nat â Stream a â Stream a
insertAt : Nat â a â Stream a â Stream a
insertEvery : Nat â a â Stream a â Stream a
takeStep : Nat â Stream a â Stream a
2023-06-17 (hw17._)
- Implement your solutions in Agda (Co.agda). (updated: 2023-06-18 21:51, local time)
2023-06-19 (hw18._)
- Prove the functoriality of products:
- $\mathrm{id}_X \times \mathrm{id}_Y = \mathrm{id}_{X\times Y}$
- $(f \circ h) \times (g \circ k) = (f \times g) \circ (h \times k)$
- Do the same for coproducts.
- Do the same for (finite) powersets.
- Î. $\mathsf{head}\,(\mathsf{tail}^{2n}\, (\mathit{merge}\; (\sigma,\tau))) = \mathsf{head}\, (\mathsf{tail}^n\, \sigma)$
- Î. $\mathsf{head}\,(\mathsf{tail}^{2n+1}\, (\mathit{merge}\; (\sigma,\tau))) = \mathsf{head}\, (\mathsf{tail}^n\, \tau)$
- Î. $\mathit{merge}\; (\mathit{evens}\; \sigma, \mathit{odds}\; \sigma) = \sigma$
- Complete the proof that [O,S] : 1 + â â â is an initial T-algebra for T(X) = 1 + X.
- Find an initial T-algebra for T(X) = 1 + AĂX and prove that it really is.
- Find an initial T-algebra for T(X) = 1 + XĂX.
- Find an initial T-algebra for the signature of semigroups and prove that it really is.
2023-07-02
- Free to study: Moschovakis on posets and fixpoints
- Free to study: Halmos, Bell & Machover on Boolean Algebras
- Free to study: Jacobs & Rutten on (co)algebras
2023-07-10 (hw19._)
- Verify that for a fixed set A, the operations $(X \mapsto X^A)$ and $(X \mapsto A^X)$ are functors, and identify which is covariant and which is contravariant.
- Prove that $a\supset b$ is an exponencial in $(\supset,\land,\top)$-IPL.
- aâb ⧠a âą b
- Give formation, introduction, and elimination rules for $(\lor)$ and $(\bot)$ (for IPL).
- Prove that đđšđŹđđ has exponentials.
- In a CCC â, what is the transpose of an evaluation $\varepsilon : B^A\times A \to B$?
- In đđđ, what is the transposeâŠ
- $\tilde 1$ of $1 : A\times B \to A\times B$;
- of $\varepsilon\circ\tau$ where $\tau : A \times B^A \to B^A\times A$ is the twist arrow $\tau = \langle p_2, p_1\rangle$.
- Reprove (elementarily, by the UMPs and diagram chasing) that in any cat with finite products:
- (Ă)-id: $A \times 1 \cong A$;
- (Ă)-com: $A \times B \cong B \times A$;
- (Ă)-ass: $(A \times B) \times C \cong A \times (B \times C)$;
- Prove (elementarily, by the UMPs and diagram chasing) that in any CCC:
- $A^1 \cong A$;
- $1^A \cong 1$;
- $(A \times B)^C \cong A^C \times B^C$;
- $A^{B\times C} \cong (A^C)^B$;
- Prove (elementarily, by the UMPs and diagram chasing) that in any bicartesian closed category (i.e.: CCC with finite coproducts):
- (+)-id: $A+0 \cong A$;
- (+)-com: $A + B \cong B + A$;
- (+)-ass: $(A + B) + C \cong A + (B + C)$;
- (Ă,+)-distr: $A\times(B+C) \cong A\times B + A\times C$;
- (Ă)-ann: $A \times 0 \cong 0$;
- $A^{B+C} \cong A^B \times A^C$;
- $A^0 \cong 1$;
- Prove that any BA âŹ, regarded as a poset cat, is a CCC.
- Definition. A Heyting Algebra (HA) is a poset with: (i) finite meets; (ii) finite joins; (iii) exponentials. Prove:
- Every HA is a distributive lattice.
- Every BA is a HA.
- Not every HA is a BA.
- $\omega\mathbf{CPO}$ is a CCC.
- $\omega\mathbf{CPO}_{\bot}$ isnât!
- Is đđšđ§đšđąđ a CCC?
- Is $\mathbf{Set_{\star}}$ (pointed sets) a CCC?
- [awodey], cap. 6â7
2023-07-17 (hw19._)
- Use the âYoneda artilleryâ to prove the arithmetic theorems of hw19.
- Prove the second corollary of Yoneda: yC â yD â C â D
- Prove the Yoneda lemma.
- [awodey], cap. 8.
2023-07-18
- Watch Riehlâs The Yoneda lemma in the category of matrices
- Free to study: anything!
Log
2023-03-06: Cancelled by UFRN
2023-03-08: Introdução
- Previously on FMCâŠ
- «Collection» vs «set»
- Definition of a category
- Examples
- đ, đ, đ, đ
- $\mathbf{Set}, \mathbf{Set}_{\mathbf{fin}}, \mathbf{Set}_{\mathbf{inj}}$
2023-03-13: Cats
- Recap: Definition of a category
- Commutative diagrams
- Algebraic structures
- Magma, Semigroup, Monoid, Group, Abel, âŠ
- Lattice, Ring, Vectâ, âŠ
- Whatâs different about Field
- $\mathbf{Set}_{(\subseteq)}$
- ${\mathbf{Nat}}_{(\mid)}$
- Objetos terminais e iniciais
2023-03-15: Cancelled by UFRN
2023-03-20: Cancelled by UFRN
2023-03-22: Cancelled by UFRN
2023-03-27: Cats
- Recap: Categorial definitions
- Constructing categories fromâŠ
- a set (discrete category)
- a pointed set
- a monoid
- a proset
- thin categories
- iso arrows, isomorphic objects
- product: definition and examples
- a new way to define what monoid and group means
2023-03-29: Cats
- from cartesian products to disjoint unions to coproducts
- the pairing of f,g: $\langle f,g \rangle$
- the copairing of f,g: $\left\{{f \atop g}\right\}.$
- mono, epi, split mono, split epi
2023-04-03: Cats
- Î. in $\mathbf{Set}$, mono implies inj
- (Ă)-assoc.
- some proofs by âdiagram chacingâ
- (Ă)-identity in $\mathbf{Set}$
- (Ă)-annihilator in $\mathbf{Set}$
- What do we mean by «â has products» (and similar phrases)
- the opposite category
- the duality principle
- some valid equations about pairing and products and how to prove them
2023-04-05: Cats
- not-so-cheap identities and inverses
- a category where A Ă 0 â A
- zero object
- retraction, section
- (â)á”á”
- comma categories: â/C, C/â
- arrow categories: $\mathbb C^{\to}$
- Functors
- forgetful functors
2023-04-10: Cats
- Q&A
- the meaning of «â has finite products»
- the non-category of Haskell, đđđŹđ€
- construction: âĂđ»
- equalizers
2023-04-12: Cats
- Equivalence relations
- Quotient set: a better definition
- Pullback: a guided definition
- Prova 1.1
2023-04-17: Cats
- Hom-sets
- The Functor Hom(A,â)
- post-composition and pre-composition
- The meaning of «best»
- The categories $\mathrm{Span}_{A,B}$ and $\mathrm{Cospan}_{A,B}$
- Preorder theory: first steps
2023-04-19: Orders
2023-04-24: Cats; Orders
- Towards a definition for natural transformations
- Ideas for composing natural transformations
- Constructions on p(r)osets
- Lift
- product with lexicographic order
- product with pointwise order
- âverticalâ sum of p(r)osets
- âhorizontalâ sum of p(r)osets
2023-04-26: Orders
- the covered-by relation
- functions between p(r)osets: order-preserving (monotone); order-embedding; order-isomorphism
- numeral posets: discrete and ordinal
- downwards-closed; upwards-closed (down-set or lower set; upper set or up-set)
- âA; âA; âx; âx
- the poset đȘ(P) of all downsets of P
- đȘ(Pâ1) â đȘ(P)â1
- đȘ(1âP) â 1âđȘ(P)
- đȘ(PâQ) â đȘ(P)ĂđȘ(Q)
2023-05-03: Orders
- Lattices
- (â„A) is an upset
- Algebraic laws of lattices: Com. Ass. Idem. Abs.
- From (L;â€) to (L;âš,â§)
- Consigo Idenp. a partir das outras trĂȘs
- NĂŁo tenho distributividade garantida
- Abordagem Algebrica (Lattice) (L;^,v) e leis
- Tradução entre as duas abordagens
- Definindo †a partir dos joinzinhos e meetzinhos
- x v y = y <=> x ^ y = x
- Sublattices e homomorfismos
2023-05-08: Orders
- Î. monotonicity of (âš) and (â§)
- Î. (â§) distributes over (âš) â (âš) distributes over (â§)
- The function space (XâP) with pointwise order
- Sub(đą) and NSub(đą)
- Î. (safe-distr)
- xâ§(yâšz) â„ (xâ§y)âš(xâ§z)
- xâš(yâ§z) †(xâšy)â§(xâšz)
- Î. (safe-modul)
- x †z â xâš(yâ§z) †(xâšy)â§z
- D. complete lattice
- C. complete â bounded
- Î. (â â : complete lattice)(â f : L â L monotone)[ f has a fixpoint ]
- âŠand even more!
2023-05-10: Orders
- Uses of the Connecting Lemma in proving inequalities
- A non-modular lattice: đâ
- Î. Distributive â Modular
- Î. The đââđâ theorem (statement and applications)
- Galois connections
- Chains and antichains
- length of a chain, length of a poset, width of a poset
2023-05-15: Prova 1.2
2023-05-17
- sublattice generated by a A â L
- top-down and bottom-up
- towards the concept of free and freely generated
2023-05-22: Freedom
- free things: free lattice, free monad, free group, free abelian group
2023-05-24: Chains
- D. (ACC), (DCC)
- Î. (ACC) â (âAâ·P)[ A has maximal ]
- Î. (DCC) â (âAâ·P)[ A has minimal ]
- Î. No infinite chains â (ACC) & (DCC)
- D. Chain-complete posets
- Î. cc â bottom
- Î. flat â cc
- Î. monotone maps preserve chains
2023-05-29: Ordinals; chain-complete posets
- about cardinal and ordinal numbers and arithmetic
- Ï + 1 â 1 + Ï = Ï
- funçÔes compatĂveis vs comparĂĄveis
- sequences: finite, longer, and even longer
- counably continuous mapping
- limit of sequence in a c.c. poset
- monotone maps preserve chains
- fixpoint theorem for countably continuous maps in c.c. posets
2023-05-31: c.c. posets of partial functions
- Î. Kleeneâs fixpoint theorem for c.c. posets and countably continuous mappings
- D. compact mapping
- âDâ. continuous mapping âââ monotone & compact
- Î. Ï : (AâE)â(BâM) continuous (characterization)
- Î. Let $S$ be an inhabited chain of $(A\rightharpoonup E)$. Let $f_0 \mathrel{\sqsubseteq_{\textrm{fin}}} \sup S$. Then there exists $s \in S$ such that $f_0 \sqsubseteq s$.
2023-06-05: Boolean Algebras
2023-06-07: Boolean Algebras
2023-06-12: BA; Recursion and corecursion
2023-06-14: BA; Recursion and corecursion
- Zornâs Lemma
- Î. Ultrafilter theorem
- Polynomial functors
- T-algebras
2023-06-19: T-ĂĄlgebras
2023-06-21: T-ĂĄlgebras
2023-06-26: T-ĂĄlgebras & T-coĂĄlgebras
2023-06-28: T-coĂĄlgebras
2023-07-03â05: Cancelled
2023-07-10: Exponentials and CCCâs
- Covariant & Contravariant functors
- Representable functors
- Exponential object
- UMPs as two-way rules of inference
- CCC (Cartesian Closed Categories)
- Arithmetic in CCCâs
- Formation, Introduction, Elimination Rules for (â,â§,â€)-IPL
- Exponential objects in â[âąIPL]
2023-07-12: CCCâs, λ-calculus, categories of functors
- From IPL with «derives» to λ-calculus with actual proof terms
- Natural transformations and natural isomorphisms
- The category ${\mathbb D}^{\mathbb C}$
- «Sets through time» as $\mathbf{Sets}^{\omega}$
- Known categories as special cases of ${\mathbb D}^{\mathbb C}$ and $\mathbf{Sets}^{{\mathbb C}^{\mathrm{op}}}$.
- $\mathbb C^2, \mathbb C^{\to}, \mathbf{Graphs}$
- Speaking of edges and vertices from within $\mathbf{Graphs}$
2023-07-17: Yoneda & applications
- Yoneda embedding
- Yoneda Lemma and corollaries
- Applications
Future
Course has ended.