```agda
module Authors where
```

# About the authors

This is a page where everyone who adds to the 1lab can write a little
bit about themselves. I mean it: everyone can write a bit about
themselves! Try to follow the format of existing profiles [in the source
file], and keep the description short. Don't forget to mention your
pronouns.

[in the source file]: https://github.com/the1lab/1lab/blob/main/src/Authors.lagda.md?plain=1

<!-- KEEP THIS SVG HERE -->

<svg width="0" height="0">
  <clipPath id="squircle" clipPathUnits="objectBoundingBox">
    <path
      fill="red"
      stroke="none"
      d="M 0,0.5 C 0,0 0,0 0.5,0 S 1,0 1,0.5 1,1 0.5,1 0,1 0,0.5"
    />
  </clipPath>
</svg>

<!-- ALTERNATE pfp-left AND pfp-right CLASSES FOR EACH PROFILE -->

<div class="profile pfp-left">
<div class="profile-pfp">
<img alt="Amélia's profile picture" src="static/pfps/amelia.png" />
<span class="profile-name">Amélia</span>
<span class="profile-pronouns">they/them</span>
<span><a href="https://twitter.com/plt_amy">\@plt_amy</a></span>
</div>

<div class="profile-profile">
Hi! I'm Amélia, a non-binary programmer/mathematician. I'm 21, but I've
been programming since age 7, and doing dependently-typed programming
since 14. Last year, I implemented [my own cubical type theory], to
figure out what it was all about.

Since then, I've realised that my energy would be better spent making
_existing_ type theories more accessible, and this project was the
result. The 1lab grew out of a personal project formalising category
theory to better my understanding of category theory, and it's currently
undergoing a rewrite from base Agda-with-K to Cubical Agda.

[my own cubical type theory]: https://git.amelia.how/amelia/cubical

My other notable projects include [my personal blog], where I write
about type theory and the implementation of programming languages, and
[Amulet], a ML-family language with an advanced type system.

[my personal blog]: https://amelia.how
[Amulet]: https://amulet.works
</div>
</div>

<div class="profile pfp-right">
<div class="profile-pfp">
<span class="profile-name">Reed</span>
<span class="profile-pronouns">he/him</span>
<span><a href="https://twitter.com/totbwf">\@totbwf</a></span>
<span><a href="https://github.com/totbwf">totbwf</a></span>
</div>

<div class="profile-profile">
Hey! I'm Reed! I develop proof assistants for a living, and write a _lot_ of Agda.
I'm interested in how we can make our tools more human friendly. In that vein,
I like writing various forms of automation, especially those with a more
semantic flavor.
</div>
</div>

<div class="profile pfp-left">
<div class="profile-pfp">
<img alt="Naïm's profile picture" src="https://www.gravatar.com/avatar/1fea7494d69948ab0a50d9ee9318ae50?s=128&r=g" />
<span class="profile-name">Naïm</span>
<span class="profile-pronouns">any</span>
<span><a href="https://monade.li">monade.li</a></span>
<span><a href="https://github.com/ncfavier">ncfavier</a></span>
</div>

<div class="profile-profile">
I'm Naïm. I like the [computational trilogy](https://ncatlab.org/nlab/show/computational+trilogy)
and arguing with Agda. I hate broken links and writing about myself.
</div>
</div>
