self study 🐈 BabyCats

Pré-sessões: warm-up

Incluo aqui 4 sessões de “warm-up”, de CFR. Nessas sessões encontramos diagramas comutativos, propriedades universais de funções e conjuntos, estilo point-free, produtos, coprodutos, pairing, copairing. Logo depois do warm-up, seguem as 3 sessões de «baby cats», encontrando as primeiras noções da teoria das categorias.

BabyCats (-4) & CFR1 (13) [video]

• Partições e coberturas de conjuntos
• Diagramas comutativos
• Leis da composição (assoc. e ident.)
• [tacit-programming][Estilo tácito] (aka: point-free, pointless)
• a função const : β → α → β e um desafio
• Uma das leis de identidade descrita como diagrama comutativo
• id é uma identidade para a composição
• recap: funções e diagramas relacionados ao produto (×)
• única função que faz um diagrama comutar
• união disjunta: no caminho de achar a soma de conjuntos
• Plicker: a ℘f respeita as uniões e as interseções?

hw

1. Seja (~) uma relação de equivalência num conjunto $A$. Para qualquer $a ∈ A$, denote por $[a]_{\sim}$ o conjunto $\{x \mid x \sim a \}$. O $\{ [a]_{\sim} \mid a \in A \}$ é uma partição do $A$?
2. Alguém definiu: «Uma partição num conjunto A é uma função …». Adivinhe o … e justifique tal frase!
3. Defina uma ordem interessante no Partition(A).
4. Demonstre que se os dois quadradinhos do diagrama da aula comutam, o diagrama todo comuta.
5. Qual deve ser a próxima pergunta para perguntar depois de descubrir que const = curry outl?
6. Demonstre as leis de composição estilo point-full.
7. Qual seria a especificação do produto?
8. Qual seria a especificação de soma?
9. Tente achar outras implementações de união-disjuntora (soma)
10. Quais seriam os diagramas e funções relacionados à união-disjuntora?
11. Melhore nossa definição de iterações de funções, e demonstre umas propriedades interessantes sobre elas.
12. Até §«Definições estilo point-free»
13. Reveja a §«Funções de graça» e seus exercícios.
14. Problemas: Π8.12; Π8.13; Π8.14; Π8.16; Π8.19; Π8.20; Π8.22

BabyCats (-3) & CFR1 (14) [video]

• Fixpoints
• Definindo iterações melhor (sem pontos)
• Mais funções de graça: pointwise, diagonal, pareamento, produto
• Uma vantagem de usar funções descurrificadas
• conjuntista-vs-tipista sobre funções (e pouco em geral)
• implementações usando funções
• funções parciais e não-deterministas
• união-disjunta: especificação-vs-implementação, copareamento, coproduto

BabyCats (-2) & CFR2 (1) [video]

• retrações e secções
• funções (L/R)-invertíveis
• funções (L/R)-canceláveis
• como dizer Seja a ∈ A. sem pontos
• confundindo aplicações com composições

hw

1. Verifique cada uma das 8 implicações:
   • f inj ⇔ f L-cancelável ⇔ f L-invertível
   • f sobre ⇔ f R-cancelável ⇔ f R-invertível
2. Capítulo «Funções»: §«Uma viagem épica»; §«Retracções e secções»

BabyCats (-1) & CFR2 (2) [video]

• especificações sem pontos
• procurando uma especificação para produto
• ganhando gratuitamente uma especificação para soma (coproduto)
• pairing, copairing, projeções, coprojeções

hw

1. Escreva sozinho as especificações de produto e de coproduto.
2. Verifique que B×A com as toA e toB que definimos, é um produto de A e B
3. o A×B×A com as toA (x,y,z) = x e toB (x,y,z) = y, é um produto de A e B?
4. Mostre que o A∪B não é um coproduto (soma) dos A e B
5. Generalize as especificações de produto e coproduto do caso binário para o caso geral, aplicável em qualquer ℐ-família de conjuntos.
6. Tente formular uma especificação para o que seria a exponenciação Bᴬ de um conjunto B elevado a um conjunto A (dica: lembra da eval?)

Sessões

🐱 BabyCats (1) & CFR2 (4) & IEA (14): [video]

• O que é uma categoria: dados (interface) e leis
• Exemplos de categorias
  • Categoria a partir dum monóide
  • Categoria a partir duma estrutura algébrica (𝐌𝐚𝐠𝐦𝐚, 𝐒𝐞𝐦𝐢𝐠𝐫𝐨𝐮𝐩, 𝐌𝐨𝐧𝐨𝐢𝐝, 𝐆𝐫𝐨𝐮𝐩, 𝐀𝐛𝐞𝐥, 𝐑𝐢𝐧𝐠, …)
  • As categorias 𝟘, 𝟙, 𝟚
  • Categoria a partir duma preordem
• Definições categoriais
  • Objeto terminal
  • Objeto inicial

hw

1. Como definarias a categoria 𝟛?
2. Como definarias a categoria 𝕟?
3. Para cada uma das categorias que encontramos, determina seus objetos iniciais e seus objetos terminais, caso existam. Caso contrário, verifique tal ausência.
   1. As categorias 𝟘, 𝟙, 𝟚, 𝟛, …
   2. A categoria ℂ[ℳ] baseada a um monóide ℳ.
   3. A categoria ℂ[(ℕ;≤)], i.e., a categoria baseada no ℕ com sua (pre)ordem canônica (≤))
   4. A categoria ℂ[(ℤ;≤)]
   5. A categoria ℂ[(ℤ;|)]
   6. A categoria ℂ[(℘S;⊆)]
   7. As categorias de umas estruturas algébricas: $\mathbf{Semigroup}$, $\mathbf{Monoid}$, $\mathbf{Group}$, $\mathbf{Abel}$, $\mathbf{Ring}$

🐱 BabyCats (2) & CFR2 (5) & IEA (15) [video]

• Definição de categoria (recap)
• Exemplos (antigos e novos)
• categorias magras (thin)
• categorias discretas
• categorias a partir de linguagens de programação
• categorias a partir de sistemas de lógica
• objetos: terminal; inicial; zero
• setas: (split) mono; (split) epi; iso
• objetos isômorfos
• Θ. os terminais são isômorfos
• categoria oposta e o princípio da dualidade
• conceitos «self-dual»
• presente da dualidade: Θ (gratuito). os iniciais são isômorfos
• produto e coproduto de dois objetos
• traduzindo e procurando produtos e coprodutos em umas categorias
• abuso do artigo definido
• diagram chasing
• Plicker: tem produtos e coprodutos na categoria 𝐆𝐫𝐨𝐮𝐩?

hw

1. Para cada uma das categorias que encontramos até agora traduza os conceitos de «produto» e «coproduto» e verifique se elas possuem ou não
2. A mesma coisa sobre os conceitos de «terminal», «inicial», «zero», já que conhecemos mais categorias desde a aula anterior
3. Verifique que a (≅) de «é isômorfo a» é uma relação de equivalências nos objetos de qualquer categoria
4. Demonstre que todos os produtos de dois objetos A,B são isômorfos («unicidade» de produtos)
5. Demonstre que todos os coprodutos de dois objetos A,B são isômorfos («unicidade» de coprodutos)
6. Tente definir categorias onde os objetos são:
   1. as categorias(!)
   2. as setas de uma data categoria ℂ

🐱 BabyCats (3) & CFR2 (6) & IEA (16) [video]

• Propriedades universais
• (≅) é uma relação de equivalência
• Uma categoria com setas matrizes
• (Re)definindo monóides, grupos, grupóides
• A categoria das setas de ℂ
• As categorias “comma”: slice ou over (ℂ/C); coslice ou under (C/ℂ)
• Functors e a categoria 𝐂𝐚𝐭
• Functors em programação funcional
• O que seriam setas entre functors?
• Plicker: A × 1 ≅ A? A × 0 ≅ 0?

hw

1. Escreva sozinho as definições categoriais que conhecemos até agora.
2. Fixe duas categorias ℂ,𝔻. Considere cada functor ℂ → 𝔻 como um objeto em uma nova categoria. Como definarias as setas nessa nova categoria?
3. Traduza os conceitos categoriais que temos definido até agora nas novas categorias que conhecemos.
4. Entre na 𝐀𝐛𝐞𝐥. Sejam 𝒜,ℬ objetos desse mundo. Mostre que o grupo abeliano 𝒜×ℬ definido usando as operações component-wise é um produto dos 𝒜,ℬ mesmo (com quais setas?). Mostre que o mesmo grupo abeliano é um coproduto dos 𝒜,ℬ (com quais setas?).
5. O 𝐑𝐢𝐧𝐠 tem inicial? Terminal?
6. Suponha que a $\mathbb C$ tem (co)produtos. A $\mathbb C^{\to}$ tem (co)produtos?
7. Investiga a existência de (co)produtos e (co)terminais nas categorias “comma” ℂ/C e C/ℂ (slice ou over; e coslice ou under).
8. Na aula encontramos maneiras de (re)definir os conceitos de monóide e de grúpo. No mesmo estilo como (re)definarias os conceitos de «homomorfismo entre monóides» e «homomorfismo entre grupos»?
9. Defina functors:
   1. De 𝐆𝐫𝐨𝐮𝐩 para 𝐌𝐨𝐧𝐨𝐢𝐝
   2. De 𝐑𝐢𝐧𝐠 para 𝐀𝐛𝐞𝐥
   3. De 𝐑𝐢𝐧𝐠 para 𝐌𝐨𝐧𝐨𝐢𝐝
   4. De 𝐌𝐨𝐧𝐨𝐢𝐝 para 𝐒𝐞𝐭
   5. De 𝐒𝐞𝐭 para 𝐌𝐨𝐧𝐨𝐢𝐝
   6. De ℂ[ℳ] para 𝐒𝐞𝐭, para uns monóides ℳ que tu gosta
   7. De ℂ[𝒢] para 𝐒𝐞𝐭, para uns grupos 𝒢 que tu gosta