❓ Frequently Asked Questions — CGPA Board FAQ

CGPA is run by a small team of mods and admins:

• PurrfectProof — Founder & Admin (she/her) — resident HoTT witch 🧙‍♀️
• ∞-Catgroupoid — Global Moderator (they/them) — Agda & Cubical specialist
• NyanLambda — Moderator (she/her) — Coq/Rocq & Lean 4 enthusiast
• MeowMonoid — Moderator (he/him) — category theory & FP
• KittyKernel — Bot / Automation — does not bite, usually

The forum is hosted on cgpa.isarabbithole.com and powered by Rabbithole.

Nope! We're a purely independent, volunteer-run community. Several members are academics, PhD students, or researchers, but CGPA is not affiliated with any institution. Discussion here represents individual members, not any organization.

That said, we do maintain a Resources page linking to official reading materials, lecture notes, and course pages from universities and research groups (all used with love and gratitude).

Click the Register link at the top of any page (or right here). Fill in your username, email, and password. Username rules:

• 3–24 characters, alphanumeric + underscores/hyphens/spaces allowed
• No impersonation of staff (e.g. don't call yourself "Admin" or "PurrfectProof")
• Unicode is fine! Many members use math symbols: ∀xCat, λNya, etc.
• Please avoid usernames that are offensive or harmful

Head to 🐾 Introductions & Mewlcome Mat and say hi! Tell us a bit about yourself: what brought you here, what you're interested in, what you're currently learning. We love meeting new members. nya~

After that, the 🌱 Beginners' Litter Box subforum is a safe, judgment-free space to ask "basic" questions about type theory, Agda, functional programming, and related topics. No question is too simple — we were all kittens once. 🐾

Great question, future type theorist! Here's the CGPA-recommended path:

1. Read the HoTT Book — available free at homotopytypetheory.org/book. It's the definitive reference for Homotopy Type Theory and Univalent Foundations.
2. Play The HoTT Game — a guided sequence of exercises in Cubical Agda. It can be played entirely in your browser via Agdapad with no local install required! There are two tracks: Fundamental Group of the Circle (shows π₁(S¹) = ℤ) and Trinitarianism (logic + type theory + category theory). CGPA recommends starting with Fundamental Group for intuition.
3. Martin Escardó's Lecture Notes — Introduction to HoTT/UF with Agda at martinescardo.github.io. Starts from scratch with explicit universe levels.
4. Install Agda locally — follow the official Agda documentation. We recommend VS Code + the agda-mode extension for a friendlier setup.
5. Join our Beginners subforum and post any questions! We have a dedicated Agda Help Megathread.

Use the BBCode [code] tag to wrap your code. For language-specific syntax highlighting, use [code=agda], [code=haskell], [code=coq], [code=lean], etc.

[code=agda]
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero  + m = m
suc n + m = suc (n + m)
[/code]

Which renders as a highlighted block. Supported languages include:

• agda, coq, lean, idris
• haskell, ocaml, sml, scala
• python, java, c, cpp, rust
• bash, json, yaml, and more

CGPA supports inline and display LaTeX via a MathJax integration. Use [math] tags:

Inline math: [math]\pi_1(S^1) \cong \mathbb{Z}[/math]

Display math (centred block):
[math display]
\sum_{n=0}^{\infty} \frac{(-1)^n}{2n+1} = \frac{\pi}{4}
[/math]

You can also use standard LaTeX environments inside display blocks:

[math display]
\begin{aligned}
  A &\simeq B \\
  &\Leftrightarrow \text{isEquiv}(f)
\end{aligned}
[/math]

Standard phpBB BBCode is fully supported:

• [b]bold[/b], [i]italic[/i], [u]underline[/u]
• [s]strikethrough[/s], [sup]superscript[/sup]
• [color=#ff79c6]pink text[/color]
• [size=14]larger text[/size]
• [url=https://example.com]link text[/url]
• [img]https://...[/img] for images (hotlinking allowed)
• [quote="username"]quoted text[/quote]
• [spoiler]hidden content[/spoiler] — click to reveal!
• [list][*]item[/list] for bullet lists

CGPA-exclusive BBCode tags:

• [proof]...[/proof] — wraps a proof in a collapsible block with a ∎ marker
• [thm]...[/thm] — theorem-style formatting
• [lemma]...[/lemma], [defn]...[/defn], [rem]...[/rem]
• [nya]text[/nya] — adds random cat emoticons around your text 😸

You can paste Unicode directly into posts — the forum is fully UTF-8. Type ∀, ∃, λ, →, ≡, ⊢, 𝒰, ∞, 🐱 — all fine!

For extended math/logic Unicode in plain-text posts (not inside [math] or code blocks), we recommend using the CGPA Unicode Helper — a searchable chart of commonly-used symbols in type theory and category theory.

The full rules are at cgpa.isarabbithole.com/rules — please read them! Here is a short summary of the most critical points:

• 🐾 Be kind. Treat all members with respect. Constructive criticism is fine; personal attacks are not.
• 🐾 No discrimination. CGPA is explicitly welcoming to people of all genders, sexualities, races, disabilities, and backgrounds. Bigotry of any kind leads to an immediate ban.
• 🐾 Stay on-topic. Post in the correct subforum. Off-topic content belongs in the 🎮 Purrloined Hours section.
• 🐾 No spam or advertising without mod approval.
• 🐾 Cite your sources. If you're sharing a proof, theorem, or code from elsewhere, link the original. Academic integrity matters here.
• 🐾 Use spoilers for long proofs or off-topic tangents within a thread.
• 🐾 English is the primary language of the main forums, but we have an International 🌍 section.

Click the 🚩 Report button at the bottom-right of any post. You'll be prompted for a brief reason — please be descriptive (e.g. "spam," "personal attack in paragraph 2," "plagiarised from [link]"). Reports are reviewed by moderators within 24 hours, usually much faster.

For urgent matters (threats, doxxing), also ping a moderator directly via PM or use the Contact Us form.

Yes! Self-promotion of genuine, relevant work is welcome in the 🎉 Project Showcase subforum. Please be honest that it's your own work. If your project is relevant to an ongoing discussion in another thread, you may link to it once in context, with a brief description.

Repeatedly plugging unrelated or commercial products across multiple threads is considered spam. When in doubt, ask a mod first.

Once your question has been answered, please mark the thread solved so others can benefit from search results! Here's how:

1. Go to your original post (the first post in the thread).
2. Click Edit on that post.
3. Click the [✔ Mark Solved] checkbox in the post options panel (below the text editor).
4. Save your edit. The thread title will automatically gain a [SOLVED] prefix and a green checkmark icon.

Alternatively, you can reply to the thread with [solved] anywhere in your post body, and the KittyKernel bot will automatically mark the thread solved for you.

Edit: Yes, you can edit your own posts at any time. Edits within 10 minutes do not show an edit notice. After 10 minutes, a small "Last edited by [username]" notice appears.

Delete: You can delete your own posts if no one has replied to them yet. Once a thread has replies, you can no longer self-delete (to prevent conversation context from disappearing). Contact a mod if you need a post removed for a good reason.

Use the Report button on your thread's first post and select "Request: Pin / Move" from the dropdown, then describe your request. Mods will evaluate whether pinning is appropriate (we try to keep pinned lists short and curated).

To move a thread to a different subforum, report it with the reason "Wrong subforum — please move to [subforum name]". We're happy to help, no judgment for posting in the wrong place!

Your rank is displayed below your username in posts. Ranks are awarded automatically based on post count plus a Reputation (nya-points) modifier. The higher your reputation, the faster you can climb — quality over quantity, nya~

nya-points (⭐) are our reputation system. Any registered member can give another member's post a ⭐ by clicking the star icon next to the post. You get 1 nya-point per ⭐ received. You can receive up to 10 nya-points per day.

nya-points affect:

• Your rank threshold (high reputation = fewer posts needed to level up)
• A "Reputation" bar displayed on your profile
• Eligibility for special roles like Proof Shepherd

Yes! Once you reach the lambda catculus rank (150+ posts), you can set a custom title in your User Control Panel → Profile → Custom Title. It replaces the automatic rank name under your username.

Custom titles must:

• Be ≤ 40 characters
• Not impersonate a staff rank (e.g. "Moderator", "Admin")
• Not violate forum rules (no slurs, harassment, etc.)
• Be in reasonably good taste (math puns and cat references are highly encouraged 🐱)

You monster. Just kidding nya~ 💜 Yes! Go to User Control Panel → Board Preferences → My Board Style and select from available themes. We currently offer:

• NyaDark (default) — the dark #1a1a2e theme you're reading now
• NyaLight — a light pastel variant with the same pink/purple accents
• Catppuccin Mocha — community-favourite dark variant with warmer tones
• Catppuccin Latte — warm light theme
• Terminal Green — classic monochrome hacker aesthetic 💚

Go to UCP → Board Preferences → Edit Notification Options. You can toggle email notifications for:

• Replies to threads you've posted in
• Replies to threads you've subscribed to
• Private messages received
• Mentions (using @username in a post)
• Reputation (nya-points) events

You can also subscribe/unsubscribe to individual threads via the Subscribe to this topic link at the bottom of any thread.

Click Forgot Password on the Login page. Enter your registered email address and a password reset link will be sent. If you no longer have access to that email, contact an admin via the Contact Us form with proof of account ownership (e.g. details only the account owner would know).

Please post in the 🛠️ Board Support & Feedback subforum with as much detail as possible:

• What you were trying to do
• What you expected to happen
• What actually happened
• Browser/OS if relevant
• Screenshot if possible

For security vulnerabilities, please do not post publicly — contact the admin team privately. We take security seriously and will credit responsible disclosure. 🐾