What part of
data Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  _,_ : (a : A) → (b : B a) → Σ A B
don't you understand?
%
A monad is just a monoid in the category of endofunctors.
%
I'm a coauthor of many category theory papers.
%
The attempt to rewrite the foundations of mathematics in terms of
category theory is evil and wrong. [...] It is our destiny to confront
Catego-fascism.
%
A coconut is just a nut.
%
Beware of bugs in the above code; I have only proved it correct, not
tried it
%
We can also make Vect into a monoidal category with direct sum as the tensor product - this may seem perverse, but it's actually very useful.
%
Richard Stallman can solve the halting problem .. in polynomial time.
%
Von intuitionistischen Einwänden sehe ich ab und stelle mich durchaus auf formalistischen Boden.
%
In vain does the chicken cross the road; Emacs is on both sides.
%
To understand monad tutorials, you really have to understand monads first.
%
It should be called schönfinkeling, but currying is tastier.
%
Machs mit universellen Eigenschaften, sonst wirds Krebs.
%
The influence of mathematics on philosophy [...] has been but profound and unfortunate.
%
The command has indeed failed with message:
"The command has not failed!"
%
Wir müssen jetzt nicht darüber diskutieren, ich habe es schon in Agda bewiesen. [ich, 2023-12-26]
%
Ich nähere mich von zwei Seiten einem "reasonable take" an -- Binäre Suche durch den Meinungsraum. [ich, 2024-01-04]
%
Open sets correspond to freudian defence mechanisms [Bernard Burgoyne?]
%
It is not analogy... This torus really exists an it is exactly the structure of the neurotic [Baltimore, 1966]
%
Man goes round in circles because the structure of man is toric [Lacan, 1976]
%
Licking a lollipop through a glass window, as they say in polish [Tadeusz Litak, 2024-01-12]
%
Für Trikategorien passt das Ganze durch sorgfältiges TeXen noch auf eine Seite [Cathérine Meusburger, 2024-01-24]
%
Wie Glaukon Sokrates fragte: "Ist es höflicher eine Einladung zu einer Feier abzulehnen
oder zu kommen und möglichst schnell wieder zu gehen?" [Philip, 2024-01-27]
%
When in doubt, walk about [ich, 2023-12-27]
%
Good. My life just got minimally simpler. [Tadeusz Litak, 2024-05-13]
%
Eine Bogensehne reißt leicht -- Aristoteles [Philip, 2024-05-20]
%
Warning: This axiom is far less innocent than it first seems!!!
%
Gloin hat ein Prolog-förmiges Loch [Philip, 2024-07-01]
%
NOFA als Abkürzung für nicht-deterministische Automaten ist doof, aber die Abkürzung für deterministische Automaten ist DOFA [ich, 2024-07-01]
%
X11-Fonts sind eben "divinely inspired" [Philip, 2024-07-01]
%
Netzwerke sind mein Fetisch [anonymous cip admin, 2024-07-01]
%
I'm high on CGI! [ich, 2024-12-20]
%
Ein kommutatives Diagramm induziert die grammatikalische Vervollständing des Satzes [ich, 2025-02-10]
%
Wieso solltest du dich selbst zitieren mit einer solch abstrus falschen Aussage [Philip, 2025-02-10 gleich danach]