+
+
+
+
+
+# just tell me how to say it please
+
+sure thing. here.
+
+```{=html}
+
+```
+ ---------------------------------------------------------------------- ----------------------------------------------------
+ {.scr .laantas}
+ ufit รพulkussarim
+ \[หufit หฮธuษซkษsหษสษชฬ\]
+ ufi--t รพulkus(i)--sa--ri--m
+ cozy--[GEN]{.abbr} midwinter--[AD]{.abbr}--[PRL]{.abbr}--[DEF]{.abbr}
+ (be) cozy during midwinter
+ ---------------------------------------------------------------------- ----------------------------------------------------
+
+```{=html}
+
+```
+# details
+
+now i am not a huge fan of putting christianity into my conlang, which
+is hopefully understandable. but having a midwinter festival sounds
+cute. the days are finally getting longer! you made it through the worst
+part! and so on. so that's what this is. i think it probably takes place
+the day after the solstice, but with several days of festivities, so
+that there is still a little overlap with the *other* winter holiday.
+it's still appropriate to say it today.
+
+## seasons
+
+ time name pron. translation
+ ---------- --------------------------------------------------------------- ------------------- ---------------------------------- -------------
+ nov--jan [{.scr .laantas}]{.lang} [igisim]{.lang} [\[หiสษsiฬ\]]{.ipa .ipa-narrow} the freeze
+ feb [{.scr .laantas}]{.lang} [susurum]{.lang} [\[หsusสroฬ\]]{.ipa .ipa-narrow} the melt
+ mar--may [{.scr .laantas}]{.lang} [ลกangubam]{.lang} [\[หสaลษกษvษฬ\]]{.ipa .ipa-narrow} the bloom
+ jun--aug [{.scr .laantas}]{.lang} [guwanแธฟ]{.lang} [\[หษกษwษnmฬฉ\]]{.ipa .ipa-narrow} the sun
+ sep--oct [{.scr .laantas}]{.lang} [santum]{.lang} [\[หsantoฬ\]]{.ipa .ipa-narrow} the rain
+
+- in between [{.scr
+ .laantas}[igisim]{.text}]{.lang} (winter) and
+ [{.scr
+ .laantas}[ลกangubam]{.text}]{.lang} (spring), the month of february
+ is considered a transition between the two,
+ [{.scr
+ .laantas}[susurum]{.text}]{.lang}.
+- as a result, [{.scr
+ .laantas}[santum]{.text}]{.lang} (autumn) is only two months long.
+- [{.scr
+ .laantas}[ลกangubam]{.text}]{.lang} comes from
+ [{.scr .laantas}[ลกani]{.text}]{.lang}
+ (flower) and [{.scr
+ .laantas}[guba]{.text}]{.lang} (grow, thrive).
+
+## putting it together
+
+the word "midwinter", without any inflections, is
+[{.scr
+.laantas}[รพulkusim]{.text}]{.lang}, which comes from
+[{.scr .laantas}[รพulku]{.text}]{.lang}
+"be deep" and [{.scr
+.laantas}[igisim]{.text}]{.lang}. unusually for lรกntas,
+[{.scr .laantas}[รพulku]{.text}]{.lang} is
+a verb, rather than a noun. why? who knows.
+
+```{=html}
+
+```
+the suffix [{.scr
+.laantas}[--sari]{.text}]{.lang} is actually a pair of two suffixes,
+which together mean through, or during. the details of the whole
+situation are
+[here](https://lang.niss.website/laantas/nouns.html#locational-cases),
+but it is a cool two-dimensional system based on a thing that can be
+found in some languages of the caucasus. the
+[{.scr .laantas}[--m]{.text}]{.lang} on the end
+(of all these words so far, actually) is "the". so the full form
+[{.scr
+.laantas}[รพulkusisarim]{.text}]{.lang} means "during midwinter", and
+that one [i]{.lang} is dropped in this phrase to give the form
+[{.scr
+.laantas}[รพulkussarim]{.text}]{.lang}.
+
+now, for [{.scr
+.laantas}[ufit]{.text}]{.lang}. there is a small, but technically
+non-zero, chance that you remember the word
+[{.scr
+.laantas}[uf``{=html}a``{=html}t]{.text}]{.lang} from
+[here](https://cohost.org/niss/post/3366713-ufat-iksaha), with the
+meaning of "warm". this is actually the same word, but a bit cutesy. it
+means cozy.
+
+the implied verb in this sentence is
+[{.scr
+.laantas}[iksaha]{.text}]{.lang}, like before. this is an auxiliary verb
+for requests. for example, if [{.scr
+.laantas}[ลกikkรบha]{.text}]{.lang} means "you are going", then
+[{.scr
+.laantas}[ลกikkรบm iksaha]{.text}]{.lang} means "please go away". the
+[--ha]{.lang} here means "you" (singular). here it's dropped because the
+phrase is long enough already to be easily understood.
+
+so in the end, you get
+[{.scr
+.laantas}[ufit รพulkussarim]{.text}]{.lang}, meaning "\[stay\] cozy
+during the midwinter".
+
+::: twocol-grid
+{width="100%"}
+
+```{=html}
+
+```
+ ---------------------------------------------------------- ----
+ {.scr .laantas}
+ รพugusim ai
+ \[หฮธuษฃษsiฬmโฟai\]
+ รพugusi--m ai
+ miwiner--[DEF]{.abbr} be
+ it crismas
+ ---------------------------------------------------------- ----
+
+```{=html}
+
+```
+{width="100%"}
+
+```{=html}
+
+```
+ ------------------------------------------------------------------ ----------------------------------------
+ {.scr .laantas}
+ ufi รพugussarim
+ \[หufi หฮธuษฃษsหษสiฬ\]
+ ufi--(t) รพugus(i)--sari--m
+ cozy--([GEN]{.abbr}) miwiner--[DURING]{.abbr}--[DEF]{.abbr}
+ merr crismas
+ ------------------------------------------------------------------ ----------------------------------------
+
+```{=html}
+
+```
+:::
+
+
+
+
+
+
diff --git a/images/crismas1.png b/images/crismas1.png
new file mode 100644
index 0000000..e7b98cd
Binary files /dev/null and b/images/crismas1.png differ
diff --git a/images/crismas2.png b/images/crismas2.png
new file mode 100644
index 0000000..7097ee9
Binary files /dev/null and b/images/crismas2.png differ
diff --git a/images/panqt.nobg.png b/images/panqt.nobg.png
new file mode 100644
index 0000000..ecdadf6
Binary files /dev/null and b/images/panqt.nobg.png differ
diff --git a/images/panqt.nobg2x.png b/images/panqt.nobg2x.png
new file mode 100644
index 0000000..7598716
Binary files /dev/null and b/images/panqt.nobg2x.png differ
diff --git a/images/panqt.png b/images/panqt.png
new file mode 100644
index 0000000..43e5080
Binary files /dev/null and b/images/panqt.png differ
diff --git a/images/panqt2x.png b/images/panqt2x.png
new file mode 100644
index 0000000..8e405cb
Binary files /dev/null and b/images/panqt2x.png differ
diff --git a/images/qt.svg b/images/qt.svg
new file mode 100644
index 0000000..a7caf28
--- /dev/null
+++ b/images/qt.svg
@@ -0,0 +1,128 @@
+
+
+
\ No newline at end of file
diff --git a/images/quox-tod.png b/images/quox-tod.png
new file mode 100644
index 0000000..b9edb50
Binary files /dev/null and b/images/quox-tod.png differ
diff --git a/images/quox.png b/images/quox.png
new file mode 100644
index 0000000..96bf9f4
Binary files /dev/null and b/images/quox.png differ
diff --git a/lang b/lang
deleted file mode 160000
index f6d1067..0000000
--- a/lang
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit f6d10672d2c621a9b812142289124e72b869d265
diff --git a/posts-wip/2023-06-05-quox.md b/posts-wip/2023-06-05-quox.md
new file mode 100644
index 0000000..2e5a53b
--- /dev/null
+++ b/posts-wip/2023-06-05-quox.md
@@ -0,0 +1,315 @@
+---
+title: intro to quox
+date: 2023-06-05
+tags: [computer, quox (language)]
+show-toc: true
+bibliography: quox.bib
+link-citations: true
+...
+
+
+
+ (this is a quox)
+
+
+hello for _a while_ now i've been working on a language called quox. the
+one-sentence, meaningless summary is "qtt and xtt mashed together".
+
+:::aside
+wow, q and x! what an amazing coincidence!
+:::
+
+but maybe i should say what those are. i'm going to _try_ to aim this at someone
+who knows normal languages. i guess we'll see how successful that is. so first,
+
+# dependent types {#dt}
+
+maybe you already know this one. skip it if you want. (maybe you know all of
+this but you came to say hi anyway. hi!)
+
+all a dependent type is is a type that is allowed to talk about run
+time values. like a dependent pair might be `(lenย :ย โ)ย ร Arrayย lenย String` for
+a length paired with an array of strings with that length. a dependent function
+with a type like `(lenย :ย โ)ย โ (xย :ย A)ย โ Arrayย lenย A` takes a length and element
+`x` as arguments, and returns an array of that many copies of `x`.
+even ~~parametric polymorphism~~ generics are a specific form of dependent type:
+you take a type as a parameter, and get to use it in the types of the other
+arguments.
+
+:::aside
+
+but i can do that in rust/c++/haskell too
+
+yeah! well, partially. in rust you can have like
+
+```rust
+fn replicate(val: A) -> [A; N] {
+ [(); N].map(|_| val.clone())
+}
+```
+
+but it's a bit more restricted:
+
+- `N` has to always be known at compile time. you can't, for example, have the
+ length come from a config file or command-line argument
+- in rust [(at the time of writing)]{.note} and c++, only certain number-ish
+ types can be used in this way. in ghc-haskell you have more choice for what
+ data can be used in types, but youโor template haskellโhave to rewrite
+ functions for the type and value level, and have "singleton" types to bridge
+ between compile time and run time
+
+so yeah, you can get some of the way there, but not completely.
+
+:::
+
+dependent types let you classify values more precisely than before, so you can
+do things like have ASTs that reflect their local variables in the type.
+
+in quox, and most uses of this technique, it's enough to just keep the _number_
+of variables in scope.
+[(there are two counts in quox; see [below](#xtt) for why.)]{.note}
+in a definition like
+
+
+
+```quox
+def backwards-plus : ฯ.โ โ ฯ.โ โ โ =
+ ฮป a b โ plus b a
+```
+
+:::aside
+
+what does all that mean
+
+- the `ฯ` before each argument means you have no restrictions on how you can
+ use it. see [below](#qtt). i want to have a default so you could just write
+ `โ โ โ โ โ`, but i can't decide what the default should _be_
+- functions are curried, which means they take their arguments one by one, like
+ in haskell or ocaml, rather than in a tuple. doing it this way makes writing
+ dependencies (and quantities) easier.
+- a function is written as `ฮป var1 var2 โ body`
+- all those funky symbols have ascii alternatives, so you if you like it better
+ you can also write
+ ```quox
+ def backwards-plus : #.Nat -> #.Nat -> Nat =
+ fun a b => plus b a
+ ```
+
+:::
+
+the right hand side `ฮป a b โ plus b a` is necessarily a `Term 0 0`, with
+no local variables. the body of the function is a `Term 0 2`, because it has two
+term variables in scope.
+
+typing contexts also know how many variables they bind, so you can know for sure
+you are keeping the context properly in sync with the term under consideration.
+and if you forget, then the compiler, uh, "reminds" you. since it's notoriously
+easy to make off-by-one errors and similar mistakes when dealing with variables,
+so having the computer check your work helps a lot.
+
+--------------------------------------------------------------------------------
+
+you might not want to have every property you will ever care about be always
+reflected in types. quox's expressions have their scope size in their type,
+because dealing with variables is ubiquitous and fiddly, but they don't have
+like, a flag for whether they're reducible. i _do_ care about that sometimes,
+but it's easier to have it as a separate value:
+
+```idris
+-- in Data.So in the standard library
+data Oh : Bool -> Type where
+ Oh : So True
+
+-- in Data.DPair (simplified for now)
+data Subset : (a : Type) -> (p : a -> Type) -> Type where
+ Element : (x : a) -> p x -> Subset a p
+
+isRedex : Definitions -> Term d n -> Bool
+
+whnf : (defs : Definitions) -> WhnfContext d n ->
+ Term d n -> Subset (Term d n) (\t => So (not (isRedex defs t)))
+```
+
+a term is a redex (reducible expression) if the top level AST node is
+something that can be immediately reduced, like a function being applied to an
+argument, or a definition that can be unfolded. whnf ([weak head
+normal form][whnf]) reduces the top of the expression until there are no more
+reductions to do, and then returns the result, along with a proof that there are
+no more.
+
+[whnf]: https://en.wikipedia.org/wiki/Lambda_calculus_definition#Weak_head_normal_form
+
+datatype arguments can be of any type, but also, data constructors can restrict
+the values of those arguments in their return types. (this is what makes them
+useful in the first place.) in this case, `So` only has one constructor, only
+usable when its argument is `True`, meaning that constructing a value of type
+`So p` is only possible if the expression `p` reduces to `True`.
+
+:::aside
+
+`So` considered harmful, or whatever
+
+in a lot of cases you need to write the property inductively, i.e., as a
+datatype, like
+
+```idris
+data NotRedex : Definitions -> Term d n -> Type
+
+-- DPair is similar to Subset
+whnf : (defs : Definitions) -> WhnfContext d n ->
+ Term d n -> DPair (Term d n) (\t => NotRedex defs t)
+```
+
+the reason for this is that it is often easier to define other functions by
+matching on the proof rather than the original term.
+
+but in this case that is not necessary and writing a function into `Bool` is
+easier.
+
+:::
+
+other parts of the compiler, like equality checking, can similarly require
+a proof that their arguments are not redexes, so that they don't have to keep
+calling `whnf` over and over, or risk wrongly failing if one argument isn't
+reduced enough.
+
+
+# qtt (quantitative type theory) {#qtt}
+
+:::note
+(idris (2) has this one too, so i can still use real examples for now)
+:::
+
+having this extra safety is nice, but it would be even nicer if it we could be
+sure it wouldn't affect run time efficiency. for a long time, dependently typed
+languages have tried to use heuristics to elide constructor fields that were
+already determined by other fields, at least as far back as 2003 [@indices].
+but these analyses are anti-modular, in that a constructor field can only be
+erased if it is not matched against _anywhere_ in the whole program.
+
+maybe we should try telling the computer what we actually want.
+
+in qtt [@qtt; @nuttin], every local variable is annotated with
+a quantity, telling us how many times we can use it at run time. in
+quox [(and idris2)]{.note}, the possible choices are `0` (not at all;
+erased), `1` (exactly once; linear), and `ฯ` (any number
+of times; unrestricted, and the default in idris and not written). if
+a variable is marked with `0`, then you can't do anything with it that would
+affect run time behaviour. for example,
+
+- you can only match on values if their type has one or zero cases. if you
+ "have" a variable of the empty type `vย :ย {}`, you're already in an unreachable
+ branch, so it's fine to abort with
+ `case0ย v returnย โฉwhateverโช ofย {ย }`.
+ if you have an erased pair, it's fine to split it up, but the two parts will
+ still be erased.
+ matching on something like `Bool` isn't possible, because the value is no
+ longer there to look at.
+
+- type signatures only exist at compile time so you can do whatever you want
+ there.
+
+- equality proofs don't have any computational behaviour (unlike in [some other
+ type theories][hott]), so [coercion](#xtt) works with an erased proof
+
+[hott]: https://homotopytypetheory.org
+
+
+as well as erasure, there is also linearity. a linear variable must be used
+exactly once in a linear context (and any number of times in an erased context,
+like in types or proofs talking about it). this is useful for things like file
+handles and other kinds of resources that have strict usage requirements. it's
+similar to passing a variable by value in rust, where after you do so, you can't
+use it yourself any more.
+
+:::aside
+there's no equivalent to borrowing inside the type system, but
+i think with a careful choice of builtins, it would be possible to do a similar
+thing in an external library.
+
+_[rust person voice]_ it would be less _ergonomic_ as library, but having
+a borrow checker inside the language would immediately blow my _complexity
+budget_. :crab:
+:::
+
+i don't have much to say about this, honestly, but ask any rust user about the
+benefits of tracking resource ownership in types.
+
+--------------------------------------------------------------------------------
+
+so where do these quantities come from? from the types, of course. a function
+type in quox, which looks like `ฯ.(x : A) โ B`, has a quantity ฯ attached,
+which describes how a function value of that type can use its argument.
+an identity function `ฮป x โ x` can have type `1.A โ A` or `ฯ.A โ A`, but not
+`0.A โ A`. and a "diagonal" function `ฮป x โ (x, x)` can only be `ฯ.A โ A ร A`.
+
+a whole definition can be erased (and if it's a definition of a type, it has to
+be, since types don't exist at run time), like
+
+```quox
+def0 TwoOfThem : โ = โ ร โ
+```
+
+finally, you can mark a specific term with a quantity. say you want to write
+a function that returns some number, plus an erased proof that it's even.
+obviously you can't mark the whole definition as erased with `def0`, since
+you want the number itself. and giving the return type as `(n : โ) ร Even n`
+makes the proof appear at run time, which might be unwanted if it's something
+big. so you can erase the second half of the pair by writing
+`(nย :ย โ)ย ร [0.ย Evenย n]`. a value of a "boxed" type `\[ฯ.ย A]` is written `\[e]`
+if `eย :ย A`. for a slightly bigger example, you might want a decidable equality
+that gives you _erased_ proofs, so you can use them in coercions, but they don't
+show up at run time.
+
+```quox
+def0 Not : ฯ.โ โ โ = ฮป A โ ฯ.A โ {}
+
+def0 Either : ฯ.โ โ ฯ.โ โ โ = โฏ -- constructors Left and Right
+
+def0 Dec : ฯ.โ โ โ = ฮป A โ Either [0. A] [0. Not A]
+
+def Yes : 0.(A : โ ) โ 0.A โ Dec A = ฮป A y โ Left [0. A] [0. Not A] [y]
+def No : 0.(A : โ ) โ 0.(Not A) โ Dec A = ฮป A n โ Right [0. A] [0. Not A] [n]
+
+def0 DecEq : ฯ.โ โ โ = ฮป A โ ฯ.(x y : A) โ Dec (x โก y : A)
+```
+
+you can also use the same construction to have some unrestricted parts of an
+otherwise linear structure.
+
+:::aside
+still missing from this story, in my opinion, is some form of compile-time
+irrelevance. a lot of the time, you don't care about the content of a proof,
+only that it is satisfied, so if division has a type like
+`divย :ย 1.โย โ 1.(dย :ย โ)ย โ 0.(NonZeroย d)ย โย โ`, you want some way to get
+`divย xย yย pโ` and `divย xย yย pโ` to always be equal, without even having to look at
+`pโ` and `pโ`. there's no way to do that yet, because it doesn't seem to fit
+into qtt cleanly. maybe a single squash type..?
+:::
+
+
+# xtt ("extensional" type theory) {#xtt}
+
+:::aside
+but not _that_ extensional type theory
+:::
+
+[@xtt]
+
+# other stuff {#misc}
+
+- crude but effective [@crude; @mugen]
+- bidirectional typechecking [@bidi]
+- ...
+
+# i still don't know how to actually write a program {.unnumbered}
+
+i know. that's ok. i'm just trying to communicate why someone might,
+hypothetically, care.
+
+did it work?
+
+# references {#ref}
diff --git a/posts-wip/2023-06-12-algorithmic-xtt.md b/posts-wip/2023-06-12-algorithmic-xtt.md
new file mode 100644
index 0000000..9ac3fa2
--- /dev/null
+++ b/posts-wip/2023-06-12-algorithmic-xtt.md
@@ -0,0 +1,1014 @@
+---
+title: an imperfect algorithmic presentation of xtt
+date: 2023-06-12
+tags: [computer, types]
+bibliography: quox.bib
+link-citations: true
+show-toc: true
+...
+
+hello everyone. as part of my language [quox] i made a typechecking algorithm
+for xtt [@xtt]. plus other stuff. but here's just the xtt part, in case anyone
+is interested.
+
+[quox]: https://git.rhiannon.website/rhi/quox
+
+- the syntax is slightly different because it uses bidirectional typing [@bidi].
+ i've tried to roll back my other arbitrary syntactic changes for this document
+ to avoid confusion though. other than subtyping instead of explicit lifting,
+ because that seemed significantly easier. to me at least.
+- this algorithm [isn't very efficient](#compute-elim-ty). it is what currently
+ exists in quox, and when i improve that stuff in future, hopefully i'll
+ remember to come back and update this post.
+- i also **haven't proven anything**, so if it's wrong, then i apologise for my
+ hubris.
+
+anyway. let's get started.
+
+# syntax
+
+mostly follows @xtt, but with a few annotations added or removed for
+bidirectional reasons.
+
+- a "term" is a type or an introduction form. it can be checked against a given
+ type.
+- an "elimination" is a string of elimination forms applied to either a variable
+ or an annotated term. its type can be synthesised.
+- substitutions take variables to _eliminations_, to preserve typeability,
+ and in this presentation, syntactic well-formedness.
+- $x, y$ denote term variables, and $๐, ๐$ denote dimension variables.
+
+:::texdefs
+$$
+\newcommand\Ceq{\Coloneqq}
+\newcommand\Or{\mathrel|}
+\newcommand\E\underline
+\newcommand\Bar{\mathrel|}
+\newcommand\Rule[3]{
+ \begin{array}{l}
+ \text{\small [#3]} \\
+ \displaystyle
+ \frac{ \begin{gather}#1\end{gather} }{ \begin{gather}#2\end{gather} }
+ \end{array}
+}
+$$
+:::
+
+$$
+\begin{aligned}
+ ฮต &\Ceq 0 \Or 1 & \text{dimension constants} \\
+ p, q &\Ceq ๐ \Or ฮต & \text{dimensions} \\
+ ฮพ &\Ceq p = q & \text{dimension constraints} \\
+ ๐ &โ โ & \text{concrete universe levels} \\
+ โ &\Ceq ๐ \Or \top & \text{judgement levels} \\
+ s, t, u, A, B, C &\Ceq
+ ๐ฐ_โ \Or
+ (x : A) โ B \Or ฮปx. s \Or
+ (x : A) ร B \Or (s, t) \Or
+ & \text{terms (incl. types)} \\
+ & \mathrel{\hphantom{\Ceq}}
+ ๐๐พ_{๐. A} \; s \; t \Or ฮป๐. s \Or
+ ๐ฏ๐ผ๐ผ๐น \Or ๐๐ฟ๐๐ฒ \Or ๐ณ๐ฎ๐น๐๐ฒ \Or \E{e} \\
+ e, f, g &\Ceq
+ x \Or
+ f \; s \Or
+ ๐ณ๐๐ \; e \Or ๐๐ป๐ฑ \; e \Or
+ f \; p \Or
+ ๐ถ๐ณ_{x. A} \; e \; ๐๐ต๐ฒ๐ป \; s \; ๐ฒ๐น๐๐ฒ \; t \Or s : A \Or
+ & \text{eliminations} \\
+ & \mathrel{\hphantom{\Ceq}}
+ [๐. A] โ^p_{p'} s \Or
+ A โ^p_{p'} s \; [q \; ๐๐ถ๐๐ต \; 0 โช ๐. tโ \Bar 1 โช ๐. tโ] \Or \\
+ & \mathrel{\hphantom{\Ceq}}
+ ๐๐๐ฐ๐ฎ๐๐ฒ_A \; e \; \left[
+ \begin{array}{lcl}
+ ๐ฐ & โช & t_๐ฐ \\
+ ฮ \; x \; y & โช & t_ฮ \\
+ ฮฃ \; x \; y & โช & t_ฮฃ \\
+ ๐๐พ \; xโ \; xโ \; x \; yโ \; yโ & โช & t_{๐๐พ} \\
+ ๐ฏ๐ผ๐ผ๐น & โช & t_{๐ฏ๐ผ๐ผ๐น}
+ \end{array}
+ \right] \\
+ ฮจ, ฮฆ &\Ceq ยท \Or ฮจ, ๐ \Or ฮจ, ฮพ & \text{cubes} \\
+ ฮ, ฮ &\Ceq ยท \Or ฮ, x: A & \text{contexts}
+\end{aligned}
+$$
+
+only real levels $๐ โ โ$ can occur in expressions. the special level $\top$ is
+for checking a type in a context where any level is accepted, for example the
+type in an annotation $s : A$.
+
+in a $๐๐๐ฐ๐ฎ๐๐ฒ$, the pattern variables are assigned this way:
+
+- for a function type $(z : A) โ B : ๐ฐ_๐$, the $ฮ $ case is taken with
+ $x โ (A : ๐ฐ_๐)$ and $y โ ((ฮปz. B) : ๐ฐ_๐ โ ๐ฐ_๐)$.
+- same for a pair type $(z : A) ร B$ and the $ฮฃ$ case.
+- for an equality type $๐๐พ_{i. A} \; s \; t : ๐ฐ_๐$:
+ - $xโ$ and $xโ$ are set to the endpoints of the type line $A$; \
+ $xโ โ (A[0/๐] : ๐ฐ_๐)$ and $xโ โ (A[1/๐] : ๐ฐ_๐)$.
+ - $x$ is an equality between them; \
+ $x โ ((ฮป๐. A) : ๐๐พ_{๐. ๐ฐ_๐} \; A[0/๐] \; A[1/๐]$.
+ - $yโ$ and $yโ$ are the terms being equated; \
+ $yโ โ (s : A[0/๐])$ and $yโ โ (t : A[1/๐])$.
+
+----
+
+:::texdefs
+$$
+\newcommand\IN{\textcolor{#60c}}
+\newcommand\OUT{\textcolor{#082}}
+$$
+:::
+
+
+
+when introducing new judgements, the [inputs]{.input} and [outputs]{.output} are
+colour coded. all judgements assume that the cube and context are well formed
+(omitted).
+
+:::rulebox
+$$
+\begin{gathered}
+\IN{ฮจ} โข \IN{p} \; ๐๐ข๐ฆ \qquad
+\IN{ฮจ} โข \IN{p} = \IN{p'} \; ๐๐ข๐ฆ
+\end{gathered}
+$$
+:::
+
+# dimension checking {#dim}
+
+the well-formedness rules are the same as in the paper. since quox uses well
+scoped de bruijn indices, every value of type `Dim d` is well formed, so they
+don't exist at all really.
+
+the equality rules are just baby's first equational theory solver.
+
+
+:::rulebox
+$$ \IN{ฮจ} \Bar \IN{ฮ} โข \IN{A} โ ๐ญ๐ฒ๐ฉ๐_{\IN{โ}} $$
+:::
+
+# type checking {#ty}
+
+$$ \Rule{}{ฮจ, 0=1 \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_โ}{ty-01} $$
+
+$$ \Rule{}{ฮจ \Bar ฮ โข ๐ฏ๐ผ๐ผ๐น โ ๐ญ๐ฒ๐ฉ๐_โ}{ty-bool} $$
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_โ \qquad
+ ฮจ \Bar ฮ, x : A โข B โ ๐ญ๐ฒ๐ฉ๐_โ
+}{
+ ฮจ \Bar ฮ โข (x : A) โ B โ ๐ญ๐ฒ๐ฉ๐_โ \\
+ ฮจ \Bar ฮ โข (x : A) ร B โ ๐ญ๐ฒ๐ฉ๐_โ
+}{ty-pi; ty-sig}
+$$
+
+$$
+\Rule{
+ ฮจ, ๐ \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_โ \qquad
+ ฮจ, ๐, ๐ = ฮต \Bar ฮ โข s_ฮต โ A
+}{
+ ฮจ \Bar ฮ โข ๐๐พ_{๐. A} \; sโ \; sโ โ ๐ญ๐ฒ๐ฉ๐_โ
+}{ty-eq}
+$$
+
+$$ \Rule{ฮจ \Bar ฮ โข e โ ๐ฐ_โ}{ฮจ \Bar ฮ โข \E e โ ๐ญ๐ฒ๐ฉ๐_โ}{ty-el} $$
+
+:::rulebox
+$$ \IN{โ} < \IN{โ'} $$
+:::
+
+for comparing levels:
+
+$$
+\Rule{๐ <_โ ๐'}{๐ < ๐'}{lvl-nat} \qquad
+\Rule{๐ โ โ}{๐ < \top}{lvl-top}
+$$
+
+
+:::rulebox
+$$ \IN{ฮจ} \Bar \IN{ฮ} โข \IN{s} โ \IN{A} $$
+:::
+
+# term checking {#chk}
+
+assumes that $ฮจ \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_\top$.
+
+$$ \Rule{}{ฮจ, 0=1 \Bar ฮ โข s โ A}{tm-01} $$
+
+[reduce the expected type to whnf](#tm-red) before trying to match against it, of
+course.
+
+$$
+\Rule{
+ ฮ โข ๐ฐ๐ก๐ง๐ \; A โฆ A' \qquad
+ ฮจ \Bar ฮ โข_w s โ A'
+}{ฮจ \Bar ฮ โข s โ A}{tm-whnf}
+$$
+
+if $s$ is syntactically a type, then defer to $๐ญ๐ฒ๐ฉ๐$ [above](#ty).
+
+$$ \Rule{ฮจ \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_โ}{ฮจ \Bar ฮ โข_w A โ ๐ฐ_โ}{tm-ty} $$
+
+otherwise:
+
+$$
+\Rule{ฮจ \Bar ฮ, x : A โข s โ B}{ฮจ \Bar ฮ โข_w ฮปx. s โ (x : A) โ B}{tm-lam}
+$$
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข s โ A \qquad
+ ฮจ \Bar ฮ โข t โ B[(t:A)/x]
+}{ฮจ \Bar ฮ โข_w (s, t) โ (x : A) ร B}{tm-pair}
+$$
+
+$$
+\Rule{
+ ฮจ, i \Bar ฮ โข s โ A \qquad
+ ฮจ, i, i = ฮต \Bar ฮ โข s = s_ฮต โ A
+}{ฮจ \Bar ฮ โข_w ฮป๐. s โ ๐๐พ_{๐. A} \; sโ \; sโ}{tm-dlam}
+$$
+
+$$
+\Rule{}{
+ ฮจ \Bar ฮ โข_w ๐๐ฟ๐๐ฒ โ ๐ฏ๐ผ๐ผ๐น \qquad ฮจ \Bar ฮ โข_w ๐ณ๐ฎ๐น๐๐ฒ โ ๐ฏ๐ผ๐ผ๐น
+}{tm-true; tm-false}
+$$
+
+:::aside
+maybe you want to make $๐๐ฟ๐๐ฒ$ and $๐ณ๐ฎ๐น๐๐ฒ$ inferrable. _in my opinion_, there are
+not that many cases where you end up having to write $๐๐ฟ๐๐ฒ : ๐ฏ๐ผ๐ผ๐น$, and, if you
+have separate term/elim syntactic classes like i do, it's not worth muddying the
+nice clean separation in e.g. $๐ฐ๐ก๐ง๐$ for this. in my onion. :onion:
+:::
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข e โ A' \qquad
+ ฮจ \Bar ฮ โข A <:_\top A'
+}{ฮจ \Bar ฮ โข \E e โ A}{tm-el}
+$$
+
+
+:::rulebox
+$$ \IN{ฮจ} \Bar \IN{ฮ} โข \IN{e} โ \OUT{A} $$
+:::
+
+# elimination synthesis {#syn}
+
+$$ \Rule{}{ฮจ, 0=1 \Bar ฮ โข e โ ๐ฏ๐ผ๐ผ๐น}{el-01} $$
+
+in an inconsistent cube, the type being returned is just a placeholder.
+in quox, the typechecker returns what is essentially a more
+fancily-typed `Maybe`, with `Nothing` iff $ฮจ โข 0=1 \; ๐๐ข๐ฆ$.
+
+$$ \Rule{x : A โ ฮ}{ฮจ \Bar ฮ โข x โ A}{el-var} $$
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข f โ (x : A) โ B \qquad
+ ฮจ \Bar ฮ โข s โ A
+}{ฮจ \Bar ฮ โข f \; s โ B[(s:A)/x]}{el-app}
+$$
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข e โ (x : A) ร B
+}{
+ ฮจ \Bar ฮ โข ๐ณ๐๐ \; e โ A \qquad
+ ฮจ \Bar ฮ โข ๐๐ป๐ฑ \; e โ B[(๐ณ๐๐ \; e)/x]
+}{el-fst; el-snd}
+$$
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข e โ ๐ฏ๐ผ๐ผ๐น \qquad
+ ฮจ \Bar ฮ, x : ๐ฏ๐ผ๐ผ๐น โข A โ ๐ญ๐ฒ๐ฉ๐_\top \\
+ ฮจ \Bar ฮ โข s โ A[(๐๐ฟ๐๐ฒ : ๐ฏ๐ผ๐ผ๐น)/x] \qquad
+ ฮจ \Bar ฮ โข t โ A[(๐ณ๐ฎ๐น๐๐ฒ : ๐ฏ๐ผ๐ผ๐น)/x]
+}{
+ ฮจ \Bar ฮ โข ๐ถ๐ณ_{x. A} \; e \; ๐๐ต๐ฒ๐ป \; s \; ๐ฒ๐น๐๐ฒ \; t โ A[e/x]
+}{el-if}
+$$
+
+:::aside
+maybe you want to make the head of $๐ถ๐ณ$ be checkable. same caveat as making
+$๐๐ฟ๐๐ฒ$/$๐ณ๐ฎ๐น๐๐ฒ$ inferrable. i just don't think $๐ถ๐ณ \; ๐๐ฟ๐๐ฒ : ๐ฏ๐ผ๐ผ๐น \; ๐๐ต๐ฒ๐ป โฏ$
+comes up often enough to worry about it.
+:::
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_\top \qquad
+ ฮจ \Bar ฮ โข s โ A
+}{
+ ฮจ \Bar ฮ โข s : A โ A
+}{el-ann}
+$$
+
+$$
+\Rule{
+ ฮจ, ๐ \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_\top \qquad
+ ฮจ โข p \qquad ฮจ โข p' \qquad
+ ฮจ \Bar ฮ โข s โ A[p/๐]
+}{
+ ฮจ \Bar ฮ โข [๐. A] โ^p_{p'} s โ A[p'/๐]
+}{el-coe}
+$$
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_\top \qquad
+ ฮจ \Bar ฮ โข s โ A \\
+ ฮจ, q=ฮต, ๐ \Bar ฮ โข t_ฮต โ A \qquad
+ ฮจ, q=ฮต, ๐, ๐=p \Bar ฮ โข t_ฮต = s โ A \\
+}{
+ ฮจ \Bar ฮ โข
+ A โ^p_{p'} s \; [q \; ๐๐ถ๐๐ต \; 0 โช ๐. tโ \Bar 1 โช ๐. tโ]
+ โ A
+}{el-comp}
+$$
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_\top \qquad
+ ฮจ \Bar ฮ โข e โ ๐ฐ_๐ \\
+ ฮจ \Bar ฮ โข t_๐ฐ โ A \qquad
+ ฮจ \Bar ฮ โข t_{๐ฏ๐ผ๐ผ๐น} โ A \\
+ ฮจ \Bar ฮ, x : ๐ฐ_๐, y : ๐ฐ_๐ โข t_ฮ โ A \qquad
+ ฮจ \Bar ฮ, x : ๐ฐ_๐, y : ๐ฐ_๐ โข t_ฮฃ โ A \\
+ ฮจ \Bar ฮ, xโ : ๐ฐ_๐, xโ : ๐ฐ_๐, x : ๐๐พ_{\_. ๐ฐ_๐} \; xโ \; xโ,
+ yโ : xโ, yโ : xโ โข t_{๐๐พ} โ A
+}{
+ ฮจ \Bar ฮ โข
+ ๐๐๐ฐ๐ฎ๐๐ฒ_A \; e \; \left[
+ \begin{array}{lcl}
+ ๐ฐ & โช & t_๐ฐ \\
+ ฮ \; x \; y & โช & t_ฮ \\
+ ฮฃ \; x \; y & โช & t_ฮฃ \\
+ ๐๐พ \; xโ \; xโ \; x \; yโ \; yโ & โช & t_{๐๐พ} \\
+ ๐ฏ๐ผ๐ผ๐น & โช & t_{๐ฏ๐ผ๐ผ๐น}
+ \end{array}\right] โ A
+}{el-tycase}
+$$
+
+
+:::rulebox
+$$ \IN ฮจ \Bar \IN ฮ โข \IN A <:_{\IN โ} \IN B $$
+:::
+
+# subtyping {#sub}
+
+$$
+\Rule{ฮจ \Bar ฮ โข A = A' โ ๐ญ๐ฒ๐ฉ๐_โ}{ฮจ \Bar ฮ โข A <:_{โ} A'}{sub-eq}
+\qquad
+\Rule{๐โ โค ๐โ < โ}{ฮจ \Bar ฮ โข ๐ฐ_{๐โ} <:_{โ} ๐ฐ_{๐โ}}{sub-univ}
+$$
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข A' <:_{โ} A \qquad
+ ฮจ \Bar ฮ โข B <:_{โ} B'
+}{
+ ฮจ \Bar ฮ โข (x : A) โ B <:_{โ} (x : A') โ B'
+}{sub-ฮ }
+\qquad
+\Rule{
+ ฮจ \Bar ฮ โข A <:_{โ} A' \qquad
+ ฮจ \Bar ฮ โข B <:_{โ} B'
+}{
+ ฮจ \Bar ฮ โข (x : A) ร B <:_{โ} (x : A') ร B'
+}{sub-ฮฃ}
+$$
+
+$$
+\Rule{
+ ฮจ \Bar ฮ โข A <:_{โ} A' \qquad
+ ฮจ \Bar ฮ โข s = s' โ A'[0/๐] \qquad
+ ฮจ \Bar ฮ โข t = t' โ A'[1/๐]
+}{
+ ฮจ \Bar ฮ โข ๐๐พ_{i.A} \; s \; t <:_{โ} ๐๐พ_{i. A'} \; s' \; t'
+}{sub-eq}
+$$
+
+
+# equality {#eq}
+
+due to boundary separation, equality is tested separately in every consistent
+corner of the cube, by generating all dimension substitutions and applying each
+one in turn. the judgements with $โข_s$ are used in each corner individually.
+
+$$
+ฯ, ฯ \Ceq ยท \Or ฯ, ฮต/๐ \qquad \text{dimension substitutions}
+$$
+
+
+:::rulebox
+$$ \OUT ฯ โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} \; \IN ฮจ $$
+:::
+
+## cube splitting
+
+in general $ฯ$ has multiple solutions, returned as a set.
+
+$$
+\Rule{}{ยท โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} \; ยท}{sd-nil}
+$$
+
+$$
+\Rule{
+ ฯ โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} \; ฮจ
+}{
+ ฯ, 0/๐ โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} (ฮจ, ๐) \\
+ ฯ, 0/๐ โ
+ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} (ฮจ, ๐, ๐=0)
+}{sd-0}
+\qquad
+\Rule{
+ ฯ โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} \; ฮจ
+}{
+ ฯ, 1/๐ โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} (ฮจ, ๐) \\
+ ฯ, 1/๐ โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} (ฮจ, ๐, ๐=1)
+}{sd-1}
+$$
+
+
+:::rulebox
+$$ \IN{ฮจ} \Bar \IN{ฮ} โข \IN{A} = \IN{A'} โ ๐ญ๐ฒ๐ฉ๐_{\IN{โ}} $$
+:::
+
+## types {#ty-eq}
+
+assumes that $ฮจ \Bar ฮ โข A โ ๐ญ๐ฒ๐ฉ๐_โ$ and $ฮจ \Bar ฮ โข A' โ ๐ญ๐ฒ๐ฉ๐_โ$.
+
+$$
+\Rule{
+ โ ฯ โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} \; ฮจ. ฮ โข_๐ฌ A[ฯ] = B[ฯ] โ ๐ญ๐ฒ๐ฉ๐_โ
+}{
+ ฮจ \Bar ฮ โข A = B โ ๐ญ๐ฒ๐ฉ๐_โ
+}{eq-ty-split}
+$$
+
+$$ \Rule{๐ < โ}{ฮ โข_๐ฌ ๐ฐ_๐ = ๐ฐ_๐ โ ๐ญ๐ฒ๐ฉ๐_โ}{eq-ty-univ} $$
+
+$$
+\Rule{
+ ฮ โข_๐ฌ A = A' โ ๐ญ๐ฒ๐ฉ๐_โ \qquad
+ ฮ, x : A โข_๐ฌ B = B' โ ๐ญ๐ฒ๐ฉ๐_โ \qquad
+}{
+ ฮ โข_๐ฌ ((x : A) โ B) = ((x : A') โ B) โ ๐ญ๐ฒ๐ฉ๐_โ \\
+ ฮ โข_๐ฌ ((x : A) ร B) = ((x : A') ร B) โ ๐ญ๐ฒ๐ฉ๐_โ
+}{eq-ty-\{ฮ ,ฮฃ\}}
+$$
+
+$$
+\Rule{
+ ฮ โข_๐ฌ A[0/๐] = A'[0/๐] โ ๐ญ๐ฒ๐ฉ๐_โ \qquad
+ ฮ โข_๐ฌ A[1/๐] = A'[1/๐] โ ๐ญ๐ฒ๐ฉ๐_โ \\
+ ฮ โข_๐ฌ s = s' โ A[0/๐] \qquad
+ ฮ โข_๐ฌ t = t' โ A[1/๐]
+}{
+ ฮ โข_๐ฌ ๐๐พ_{i. A} \; s \; t = ๐๐พ_{i. A'} \; s' \; t' โ ๐ญ๐ฒ๐ฉ๐_โ
+}{eq-ty-eq}
+$$
+
+$$ \Rule{}{ฮ โข_๐ฌ ๐ฏ๐ผ๐ผ๐น = ๐ฏ๐ผ๐ผ๐น โ ๐ญ๐ฒ๐ฉ๐_โ}{eq-ty-bool} $$
+
+$$ \Rule{ฮ โข_๐ฌ e = e' โ ๐ฐ_๐}{ฮ โข_๐ฌ \E{e} = \E{e'} โ ๐ญ๐ฒ๐ฉ๐_๐}{eq-ty-el} $$
+
+
+:::rulebox
+$$
+\begin{gathered}
+\IN{ฮจ} \Bar \IN{ฮ} โข \IN{s} = \IN{s'} โ \IN{A} \\
+\IN{ฮ} โข_๐ฌ \IN{s} = \IN{s'} โ \IN{A}
+\end{gathered}
+$$
+:::
+
+## terms {#tm-eq}
+
+assumes that $ฮจ \Bar ฮ โข s โ A$ and $ฮจ \Bar ฮ โข s' โ A$.
+
+$$
+\Rule{
+ โ ฯ โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} \; ฮจ. ฮ โข_๐ฌ s[ฯ] = s'[ฯ] โ A[ฯ]
+}{
+ ฮจ \Bar ฮ โข s = s' โ A
+}{eq-tm-split}
+$$
+
+$$
+\Rule{
+ ฮ โข A \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐
+}{
+ ฮ โข_๐ฌ s = t โ A
+}{eq-tm-subsing}
+$$
+
+### types
+
+$$ \Rule{ฮ โข_๐ฌ s = t โ ๐ญ๐ฒ๐ฉ๐_๐}{ฮ โข_๐ฌ s = t โ ๐ฐ_๐}{eq-tm-ty} $$
+
+### functions
+
+$$
+\Rule{
+ ฮ, x : A โข_๐ฌ s = t โ B
+}{
+ ฮ โข_๐ฌ (ฮปx. s) = (ฮปx. t) โ (x : A) โ B
+}{eq-tm-ฮป}
+$$
+
+$$
+\Rule{
+ ฮ, x : A โข_๐ฌ s = \E{e \; x} โ B
+}{
+ ฮ โข_๐ฌ (ฮปx. s) = \E e โ (x : A) โ B
+}{eq-tm-ฮป-ฮท1}
+\qquad
+\Rule{
+ ฮ, x : A โข_๐ฌ \E{e \; x} = s โ B
+}{
+ ฮ โข_๐ฌ \E e = (ฮปx. s) โ (x : A) โ B
+}{eq-tm-ฮป-ฮท2}
+$$
+
+### pairs
+
+$$
+\Rule{
+ ฮ โข_๐ฌ sโ = tโ โ A \qquad
+ ฮ, x : A โข_๐ฌ sโ = tโ โ B[sโ/x]
+}{
+ ฮ โข (sโ, sโ) = (tโ, tโ) โ (x : A) ร B
+}{eq-tm-pair}
+$$
+
+$$
+\Rule{
+ ฮ โข_๐ฌ sโ = \E{๐ณ๐๐ \; e} โ A \qquad
+ ฮ โข_๐ฌ sโ = \E{๐๐ป๐ฑ \; e} โ B[sโ/x]
+}{
+ ฮ โข (sโ, sโ) = \E e โ (x : A) ร B
+}{eq-tm-pair-ฮท1}
+$$
+
+$$
+\Rule{
+ ฮ โข_๐ฌ \E{๐ณ๐๐ \; e} = tโ โ A \qquad
+ ฮ โข_๐ฌ \E{๐๐ป๐ฑ \; e} = tโ โ B[tโ/x]
+}{
+ ฮ โข \E e = (tโ, tโ) โ (x : A) ร B
+}{eq-tm-pair-ฮท2}
+$$
+
+### equalities
+
+look! uip!
+
+$$ \Rule{}{ฮ โข_๐ฌ sโ = sโ โ ๐๐พ_{i. A} \; tโ \; tโ}{eq-tm-dฮป} $$
+
+### bool
+
+$$
+\Rule{}{ฮ โข_๐ฌ ๐๐ฟ๐๐ฒ = ๐๐ฟ๐๐ฒ โ ๐ฏ๐ผ๐ผ๐น}{eq-tm-true} \qquad
+\Rule{}{ฮ โข_๐ฌ ๐ณ๐ฎ๐น๐๐ฒ = ๐ณ๐ฎ๐น๐๐ฒ โ ๐ฏ๐ผ๐ผ๐น}{eq-tm-false}
+$$
+
+### eliminations
+
+$$ \Rule{ฮ โข_๐ฌ e = e' โ A}{ฮ โข_๐ฌ \E e = \E{e'} โ A}{eq-tm-el} $$
+
+
+:::rulebox
+$$
+\begin{gathered}
+\IN{ฮจ} \Bar \IN{ฮ} โข \IN{e} = \IN{e'} \\
+\IN{ฮ} โข_๐ฌ \IN{e} = \IN{e'} โ \OUT{A}
+\end{gathered}
+$$
+:::
+
+## eliminations {#el-eq}
+
+assumes that $ฮจ \Bar ฮ โข e โ A$ and $ฮจ \Bar ฮ โข e' โ A$ for some $A$.
+
+$$
+\Rule{
+ โ ฯ โ ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐ข๐ฆ} \; ฮจ. โA. ฮ โข_๐ฌ e[ฯ] = e'[ฯ] โ A
+}{
+ ฮจ \Bar ฮ โข e = e'
+}{eq-el-split}
+$$
+
+$$
+\Rule{
+ ฮ โข ๐ญ๐ฒ \; e โฆ A \qquad ฮ โข A \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐
+}{
+ ฮ โข_๐ฌ e = e' โ A
+}{eq-el-subsing}
+$$
+
+:::aside
+the type computed for this rule can't be shared with the rest of the rules,
+because they only return a type when they succeed. very unsatisfying
+:::
+
+$$ \Rule{(x : A) โ ฮ}{ฮ โข_๐ฌ x = x โ A}{eq-el-var} $$
+
+$$
+\Rule{
+ ฮ โข_๐ฌ f = f' โ (x : A) โ B \qquad
+ ฮ โข_๐ฌ s = s' โ A
+}{
+ ฮ โข_๐ฌ f \; s = f' \; s' โ B[s/x]
+}{eq-el-app}
+$$
+
+$$
+\Rule{
+ ฮ โข_๐ฌ e = e' โ (x : A) ร B
+}{
+ ฮ โข_๐ฌ ๐ณ๐๐ \; e = ๐ณ๐๐ \; e' โ A \\
+ ฮ โข_๐ฌ ๐๐ป๐ฑ \; e = ๐๐ป๐ฑ \; e' โ B[๐ณ๐๐ \; e/x]
+}{eq-el-\{fst,snd\}}
+$$
+
+$$
+\Rule{
+ ฮ, x : ๐ฏ๐ผ๐ผ๐น โข_๐ฌ A = A' โ ๐ญ๐ฒ๐ฉ๐_\top \qquad
+ ฮ โข_๐ฌ e = e' โ ๐ฏ๐ผ๐ผ๐น \\
+ ฮ โข_๐ฌ s = s' โ A[(๐๐ฟ๐๐ฒ : ๐ฏ๐ผ๐ผ๐น)/x] \qquad
+ ฮ โข_๐ฌ t = t' โ A[(๐ณ๐ฎ๐น๐๐ฒ : ๐ฏ๐ผ๐ผ๐น)/x]
+}{
+ ฮ โข_๐ฌ ๐ถ๐ณ_{x.A} \; e \; ๐๐ต๐ฒ๐ป \; s \; ๐ฒ๐น๐๐ฒ \; t =
+ ๐ถ๐ณ_{x.A'} \; e' \; ๐๐ต๐ฒ๐ป \; s' \; ๐ฒ๐น๐๐ฒ \; t' โ A[e/x]
+}{eq-el-if}
+$$
+
+TODO coe
+
+in an empty cube, there are no dimension applications or compositions.
+
+
+:::rulebox
+$$ \IN ฮ โข \IN A \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐ $$
+:::
+
+# subsingleton types
+
+if a type is a subsingleton (only ever has zero or one possible
+values), then skip the equality check for its elements. this is used for neutral
+terms e.g. two bound variables of the same equality type.
+
+$$
+\Rule{
+ ฮ โข ๐ฐ๐ก๐ง๐ \; A โฆ A' \qquad
+ ฮ โข A' \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐ _๐ฐ
+}{ฮ โข A \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐ }{subsing}
+$$
+
+$$
+\Rule{}{
+ ฮ โข ๐๐พ_{i. A} \; s \; t \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐ _๐ฐ
+}{subsing-eq}
+$$
+
+$$
+\Rule{
+ ฮ, x : A โข B \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐
+}{
+ ฮ โข (x : A) โ B \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐ _๐ฐ
+}{subsing-ฮ }
+\qquad
+\Rule{
+ ฮ โข A \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐ \qquad
+ ฮ, x : A โข B \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐
+}{
+ ฮ โข (x : A) ร B \; ๐ฌ๐ฎ๐๐ฌ๐ข๐ง๐ _๐ฐ
+}{subsing-ฮฃ}
+$$
+
+
+# reduction {#red}
+
+:::rulebox
+$$ \IN{ฮ} โข ๐ฐ๐ก๐ง๐ \; \IN{s} โฆ \OUT{s'} $$
+:::
+
+## terms {#tm-red}
+
+assumes that $s$ is well-typed (in some consistent cube).
+
+types and introduction forms are already in whnf. so the only case non-trivial
+case is for embedded eliminations.
+
+$$
+\Rule{ฮ โข ๐ฐ๐ก๐ง๐ \; e โฆ e'}{ฮ โข ๐ฐ๐ก๐ง๐ \; \E e โฆ \E{e'}}{whnf-embed}
+\qquad
+\Rule{\text{$t$ is not an elimination}}{ฮ โข ๐ฐ๐ก๐ง๐ \; t โฆ t}{whnf-none}
+$$
+
+
+:::rulebox
+$$
+\begin{gathered}
+\IN{ฮ} โข ๐ฐ๐ก๐ง๐ \; \IN{e} โฆ \OUT{e'} \\
+\IN{ฮ} โข \IN{e} โ \OUT{e'}
+\end{gathered}
+$$
+:::
+
+## eliminations {#el-red}
+
+assumes that $e$ is well-typed (in some consistent cube).
+
+keep stepping the outermost expression until no more rules apply.
+
+$$ \Rule{ฮ โข e โ^! e'}{ฮ โข ๐ฐ๐ก๐ง๐ \; e โฆ e'}{whnf-el} $$
+
+### function application
+
+$$ \Rule{ฮ โข e โ e'}{ฮ โข e \; t โ e' \; t}{step-app-head} $$
+
+$$
+\Rule{}{
+ ฮ โข ((ฮปx. t) : (x : A) โ B) \; s โ (t[(s:A)/x] : B[(s:A)/x])
+}{step-app-ฮฒ}
+$$
+
+$$
+\Rule{
+ ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_ฮ \; x \; C โฆ (A, B) \qquad
+ ๐ฅ๐๐ญ \; \hat{s}[๐] โ [๐. A] โ^q_๐ s
+}{
+ ฮ โข (([๐. C] โ^p_q s) \; t) โ
+ [๐. B[\hat{s}[i]/x]] โ^p_q ((t : C[p/๐]) \; \hat{s}[p])
+}{step-app-coe}
+$$
+
+where $\IN ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_ฮ \; \IN{x} \; \IN{C} โฆ (\OUT A, \OUT B)$ is:
+
+$$ \Rule{}{ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_ฮ \; x \; ((y : A) โ B) โฆ (A, B[x/y])}{split-ฮ -con} $$
+
+$$
+\Rule{
+ ฮ โข ๐ญ๐ฒ \; e โฆ ๐ฐ_๐ \\
+ ๐ฅ๐๐ญ \; A โ ๐๐๐ฐ๐ฎ๐๐ฒ_{๐ฐ_๐} \; e \; [ฮ \; x \; \_ โช x \Bar \_ โช ๐ฏ๐ผ๐ผ๐น] \\
+ ๐ฅ๐๐ญ \; B โ ๐๐๐ฐ๐ฎ๐๐ฒ_{๐ฐ_๐} \; e \; [ฮ \; \_ \; y โช y \Bar \_ โช ๐ฏ๐ผ๐ผ๐น]
+}{
+ ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_ฮ \; x \; \E e โฆ (A, B \; x)
+}{split-ฮ -neut}
+$$
+
+$A$ lives in $ฮ$ and $B$ lives in $(ฮ, x:A)$.
+
+### pair projections
+
+$$
+\Rule{ฮ โข e โ e'}{
+ ฮ โข ๐ณ๐๐ \; e โ ๐ณ๐๐ \; e' \qquad
+ ฮ โข ๐๐ป๐ฑ \; e โ ๐๐ป๐ฑ \; e'
+}{step-\{fst,snd\}-head}
+$$
+
+$$
+\Rule{}{
+ ฮ โข ๐ณ๐๐ ((s, t) : (x : A) ร B) โ (s : A) \\
+ ฮ โข ๐๐ป๐ฑ ((s, t) : (x : A) ร B) โ (t : B[s/x])
+}{step-\{fst,snd\}-ฮฒ}
+$$
+
+$$
+\Rule{
+ ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_ฮฃ \; x\ ; C โฆ (A, B)
+}{
+ ฮ โข ๐ณ๐๐ ([๐. C] โ^p_q s) โ [๐. A] โ^p_q ๐ณ๐๐ \; (s : A[p/๐])
+}{step-fst-coe}
+$$
+
+$\IN ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_ฮฃ \; \IN{x} \; \IN{C} โฆ (\OUT A, \OUT B)$ is:
+
+$$
+\Rule{}{
+ ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_ฮฃ \; x \; ((y : A) ร B) โฆ (A, B[x/y])
+}{split-ฮฃ-con}
+\qquad
+\Rule{
+ ฮ โข ๐ญ๐ฒ \; e โฆ ๐ฐ_๐ \\
+ ๐ฅ๐๐ญ \; A โ ๐๐๐ฐ๐ฎ๐๐ฒ_{๐ฐ_๐} \; e \; [ฮฃ \; x \; y โช x \Bar \_ โช ๐ฏ๐ผ๐ผ๐น] \\
+ ๐ฅ๐๐ญ \; B โ ๐๐๐ฐ๐ฎ๐๐ฒ_{๐ฐ_๐} \; e \; [ฮฃ \; x \; y โช y \Bar \_ โช ๐ฏ๐ผ๐ผ๐น]
+}{
+ ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_ฮฃ \; x \; \E e โฆ (A, B \; x)
+}{split-ฮฃ-neut}
+$$
+
+$A$ lives in $ฮ$ and $B$ lives in $(ฮ, x:A)$.
+
+### dimension application
+
+$$ \Rule{ฮ โข e โ e'}{ฮ โข e \; p โ e' \; p}{step-dapp-head} $$
+
+$$
+\Rule{}{
+ ฮ โข ((ฮป๐. t) : ๐๐พ_{๐. A} \; sโ \; sโ) \; ฮต โ (s_ฮต : A[ฮต/๐])
+}{step-dapp-ฮฒ-end}
+$$
+
+$$
+\Rule{}{
+ ฮ โข ((ฮป๐. t) : ๐๐พ_{๐. A} \; sโ \; sโ) \; ๐ โ (t[๐/๐] : A[๐/๐])
+}{step-dapp-ฮฒ-var}
+$$
+
+$$
+\Rule{
+ ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐พ} \; ๐ \; C โฆ (Aโ, Aโ, A, sโ, sโ)
+}{
+ ฮ โข ([๐. C] โ^p_{p'} t) \; q โ
+ [๐. A[q/๐]] โ^p_{p'} (t : (๐๐พ_{๐.A} \; sโ \; sโ)[p/๐]) \;
+ [q \; ๐๐ถ๐๐ต \; 0 โช ๐. sโ \Bar 1 โช ๐. sโ]
+}{step-dapp-coe}
+$$
+
+this heterogeneous composition is defined in @xtt in terms of composition and
+coercion.
+$\IN ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐พ} \; \IN ๐ \; \IN C โฆ
+ (\OUT{Aโ}, \OUT{Aโ}, \OUT A, \OUT{sโ}, \OUT{sโ})$
+is:
+
+$$
+\Rule{}{
+ ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐พ} \; ๐ \; (๐๐พ_{j. A} \; sโ \; sโ) โฆ
+ (A[0/๐], A[1/๐], A[๐/๐], sโ, sโ)
+}{split-Eq-con}
+$$
+
+$$
+\Rule{
+ ฮ โข ๐ญ๐ฒ \; e โฆ ๐ฐ_๐ \\
+ ๐ฅ๐๐ญ \; Aโ โ ๐๐๐ฐ๐ฎ๐๐ฒ_{๐ฐ_๐} \; e \;
+ [๐๐พ \; aโ \; aโ \; a \; xโ \; xโ โช aโ \Bar \_ โช ๐ฏ๐ผ๐ผ๐น] \\
+ ๐ฅ๐๐ญ \; Aโ โ ๐๐๐ฐ๐ฎ๐๐ฒ_{๐ฐ_๐} \; e \;
+ [๐๐พ \; aโ \; aโ \; a \; xโ \; xโ โช aโ \Bar \_ โช ๐ฏ๐ผ๐ผ๐น] \\
+ ๐ฅ๐๐ญ \; A โ ๐๐๐ฐ๐ฎ๐๐ฒ_{๐ฐ_๐} \; e \;
+ [๐๐พ \; aโ \; aโ \; a \; xโ \; xโ โช a \Bar \_ โช ๐ฏ๐ผ๐ผ๐น] \\
+ ๐ฅ๐๐ญ \; sโ โ ๐๐๐ฐ๐ฎ๐๐ฒ_{๐ฐ_๐} \; e \;
+ [๐๐พ \; aโ \; aโ \; a \; xโ \; xโ โช xโ \Bar \_ โช ๐ฏ๐ผ๐ผ๐น] \\
+ ๐ฅ๐๐ญ \; sโ โ ๐๐๐ฐ๐ฎ๐๐ฒ_{๐ฐ_๐} \; e \;
+ [๐๐พ \; aโ \; aโ \; a \; xโ \; xโ โช xโ \Bar \_ โช ๐ฏ๐ผ๐ผ๐น]
+}{
+ ฮ โข ๐ฌ๐ฉ๐ฅ๐ข๐ญ_{๐๐พ} \; ๐ \; \E e โฆ (Aโ, Aโ, A \; ๐, sโ, sโ)
+}{split-Eq-neut}
+$$
+
+if $C$ lives in some cube $ฮจ$, then $A$ lives in $(ฮจ, i)$, and the others
+live in $ฮจ$.
+
+### conditional
+
+$$
+\Rule{ฮ โข e โ e'}{
+ ฮ โข ๐ถ๐ณ_{x. A} \; e \; ๐๐ต๐ฒ๐ป \; sโ \; ๐ฒ๐น๐๐ฒ \; sโ โ
+ ๐ถ๐ณ_{x. A} \; e' \; ๐๐ต๐ฒ๐ป \; sโ \; ๐ฒ๐น๐๐ฒ \; sโ}{step-if-head}
+$$
+
+$$
+\Rule{}{
+ ฮ โข ๐ถ๐ณ_{x. A} \; ๐๐ฟ๐๐ฒ:๐ฏ๐ผ๐ผ๐น \; ๐๐ต๐ฒ๐ป \; sโ \; ๐ฒ๐น๐๐ฒ \; sโ โ
+ (sโ : A[(๐๐ฟ๐๐ฒ:๐ฏ๐ผ๐ผ๐น)/x]) \\
+ ฮ โข ๐ถ๐ณ_{x. A} \; ๐ณ๐ฎ๐น๐๐ฒ:๐ฏ๐ผ๐ผ๐น \; ๐๐ต๐ฒ๐ป \; sโ \; ๐ฒ๐น๐๐ฒ \; sโ โ
+ (sโ : A[(๐ณ๐ฎ๐น๐๐ฒ:๐ฏ๐ผ๐ผ๐น)/x])
+}{step-if-true; step-if-false}
+$$
+
+$$
+\Rule{}{
+ ฮ โข ๐ถ๐ณ_{x.A} \; [๐.C] โ^p_q t \; ๐๐ต๐ฒ๐ป \; sโ \; ๐ฒ๐น๐๐ฒ \; sโ โ
+ ๐ถ๐ณ_{x.A} \; t : ๐ฏ๐ผ๐ผ๐น \; ๐๐ต๐ฒ๐ป \; sโ \; ๐ฒ๐น๐๐ฒ \; sโ
+}{step-if-coe}
+$$
+
+if the expression is well-typed, as we are assuming, then $C$ can only be
+something that reduces to $๐ฏ๐ผ๐ผ๐น$.
+
+
+### coercion
+
+$$
+\Rule{ฮ โข e โ e'}{ฮ โข [๐. \E e] โ^p_q s โ [๐. \E{e'}] โ^p_q s}{step-coe-ty}
+\qquad
+\Rule{๐ โ ๐๐๐ฏ \; C}{ฮ โข [๐. C] โ^p_q s โ s : C}{step-coe-non}
+$$
+
+### composition
+
+$$
+\Rule{}{ฮ โข C โ^p_p s \; [q \; ๐๐ถ๐๐ต โฏ] โ s : C}{step-comp-id}
+$$
+
+$$
+\Rule{}{
+ ฮ โข A โ^p_{p'} s \; [ฮต \; ๐๐ถ๐๐ต \; 0 โช ๐.sโ \Bar 1 โช ๐.sโ] โ
+ s_ฮต[p'/๐] : A
+}{step-comp-end}
+$$
+
+### type case
+
+$$
+\Rule{ฮ โข e โ e'}{
+ ฮ โข ๐๐๐ฐ๐ฎ๐๐ฒ_C \; e \; [โฏ] โ ๐๐๐ฐ๐ฎ๐๐ฒ_C \; e' \; [โฏ]
+}{step-tycase-head}
+$$
+
+$$
+\Rule{}{
+ ฮ โข ๐๐๐ฐ๐ฎ๐๐ฒ_C \; ๐ฏ๐ผ๐ผ๐น:๐ฐ_๐ \; [๐ฏ๐ผ๐ผ๐น โช s \Bar โฏ] โ s : C \\
+ \begin{split}
+ ฮ โข ๐๐๐ฐ๐ฎ๐๐ฒ_C \; ((x : A) โ B) : ๐ฐ_๐ \; [ฮ \; x \; y โช s \Bar โฏ] \\
+ {} โ s[(A:๐ฐ_๐)/x, ((ฮปx. B) : ๐ฐ_๐ โ ๐ฐ_๐)/y] : C
+ \end{split} \\
+ \text{etc}
+}{step-tycase-bool; etc}
+$$
+
+### annotation
+
+$$
+\Rule{}{ฮ โข \E e : A โ e}{step-ann-nest}
+\qquad
+\Rule{ฮ โข e โ e'}{ฮ โข s : \E e โ s : \E{e'}}{step-ann-ty}
+$$
+
+
+:::rulebox
+$$ \IN ฮ โข ๐ญ๐ฒ \; \IN e โฆ \OUT A $$
+:::
+
+## compute elim type {#compute-ty}
+
+assumes $ฮจ \Bar ฮ โข e โ A$ for some $ฮจ$, and just recovers the $A$ without
+doing any other checking.
+
+:::aside
+yeah. im trying to remove it
+
+- __why not just pass the type in?__ \
+ that gets you e.g. the type of $f \; s$, but that isn't enough information to
+ know the type of $f$
+:::
+
+$$ \Rule{(x : A) โ ฮ}{ฮ โข ๐ญ๐ฒ \; x โฆ A}{rety-var} $$
+
+$$
+\Rule{
+ ฮ โข ๐ญ๐ฒ \; f โฆ (x : A) โ B
+}{
+ ฮ โข ๐ญ๐ฒ (f \; s) โฆ B[(s:A)/x]
+}{rety-app}
+\qquad
+\Rule{
+ ฮ โข ๐ญ๐ฒ \; e โฆ (x : A) ร B
+}{
+ ฮ โข ๐ญ๐ฒ (๐ณ๐๐ \; e) โฆ A \\
+ ฮ โข ๐ญ๐ฒ (๐๐ป๐ฑ \; e) โฆ B[(๐ณ๐๐ \; e)/x]
+}{rety-\{fst,snd\}}
+$$
+
+$$
+\Rule{
+ ฮ โข ๐ญ๐ฒ \; f โฆ ๐๐พ_{๐.A} \; s \; t
+}{
+ ฮ โข ๐ญ๐ฒ (f \; p) โฆ A[p/๐]
+}{rety-dapp}
+\qquad
+\Rule{}{
+ ฮ โข ๐ญ๐ฒ (๐ถ๐ณ_{x.A} \; e \; ๐๐ต๐ฒ๐ป \; s \; ๐ฒ๐น๐๐ฒ \; t) โฆ A[e/x]
+}{rety-if}
+$$
+
+$$
+\Rule{}{
+ ฮ โข ๐ญ๐ฒ ([๐.C] โ^p_q s) โฆ C[q/๐]
+}{rety-coe}
+\qquad
+\Rule{}{
+ ฮ โข ๐ญ๐ฒ (A โ^p_{p'} s \; [q \; ๐๐ถ๐๐ต โฏ]) โฆ A
+}{rety-comp}
+$$
+
+$$
+\Rule{}{
+ ฮ โข ๐ญ๐ฒ (๐๐๐ฐ๐ฎ๐๐ฒ_A \; e \; [โฏ]) โฆ A
+}{rety-tycase}
+$$
+
+
+# references {#refs}
diff --git a/posts-wip/2023-10-25-quox.md b/posts-wip/2023-10-25-quox.md
new file mode 100644
index 0000000..e792b2e
--- /dev/null
+++ b/posts-wip/2023-10-25-quox.md
@@ -0,0 +1,112 @@
+---
+title: quox. the language
+date: 2023-10-25
+tags: [quox, computer, types]
+bibliography: quox.bib
+link-citations: true
+show-toc: true
+...
+
+
+
+
+:::{.aside .floating}
+### [hot minute][wkt] *n.* {.unnumbered}
+
+1. A long period of time.
+2. A short period of time.
+3. An unspecified period of time.
+
+[wkt]: https://en.wiktionary.org/wiki/hot_minute
+:::
+
+for the last _hot minute_ [@hotminute], iโve been working on a little programming language. itโs finally starting to approach a state where it can compile some programs, so maybe i should talk about it a bit.
+
+
+# what is a quox [(tl;dr for type system nerds)]{.note}
+
+
+
+ this is also a quox.
+
+
+0. itโs a *dependently typed functional language*, like your agdas and your idrises.
+1. *[q]{.qtt-q}uantitative type theory* (qtt) [@nuttin; @qtt] is a nice combination of dependent types, resource tracking, and erasure of stuff like proofs.
+2. it uses *[x]{.xtt-x}tt* [@xtt] for equality. i think it's neat
+3. it has a *closed type universe*. you donโt define new datatypes, but the language gives you building blocks to put them together. this is because of xtt originally, but i just ran with it.
+
+so now you can see where the name [q]{.qtt-q}uo[x]{.xtt-x} comes from. other than my favourite dragon. anyway it also has
+
+4. *bidirectional type checking* [@bidi]
+5. crude-but-effective stratification [@crude; @crude-blog] for dealing with universes
+
+
+# dependent types
+
+
+
+
+ sometimes i am also a quox. or three, depending on how you count.
+
+
+
+there are lots of languages with dependent types already. if you are reading this, chances are probably _quite_ high you already know what they are and can skip to the next section.
+
+`*but still something. probably*`
+
+
+# qtt
+
+sometimes, values can only be used in certain ways to make sense. this isn't controversial: it's the old use-after-free.
+
+
+# xtt
+
+
+# references {#refs}
diff --git a/posts-wip/2023-10-25-quox.md.old b/posts-wip/2023-10-25-quox.md.old
new file mode 100644
index 0000000..536dd69
--- /dev/null
+++ b/posts-wip/2023-10-25-quox.md.old
@@ -0,0 +1,177 @@
+---
+title: quox. the language
+date: 2023-10-25
+tags: [quox, computer, types]
+bibliography: quox.bib
+link-citations: true
+show-toc: true
+...
+
+
+
+
+:::{.aside .floating}
+### [hot minute](https://en.wiktionary.org/wiki/hot_minute) n. {.unnumbered}
+
+1. A long period of time.
+2. A short period of time.
+3. An unspecified period of time.
+:::
+
+for the last _hot minute_ [@hotminute], iโve been working on a little programming language. itโs finally starting to approach a state where it can compile some programs, so maybe i should talk about it a bit.
+
+
+# what is a quox [(tl;dr for type system nerds)]{.note}
+
+
+
+ this is also a quox.
+
+
+0. itโs a *dependently typed functional language*, like your agdas and your idrises.
+1. it has a *closed type universe*. you donโt define new datatypes, but the language gives you building blocks to put them together.
+2. *[q]{.qtt-q}uantitative type theory* (qtt) [@nuttin; @qtt] is a nice combination of dependent types, resource tracking, and erasure of stuff like proofs.
+3. *[x]{.xtt-x}tt* [@xtt], which `*i sure hope i remember to come back and add this!*`
+ - the closed type universe is a consequence of xtt (as well as its kinda-predecessor ott [@ott-now]), but i decided to just run with it.
+ - โxttโ stands for โextensional type theoryโ, but itโs not _that_ extensional type theory. i know. not my fault.
+
+so now you can see where the name [q]{.qtt-q}uo[x]{.xtt-x} comes from. other than my favourite dragon. anyway it also has
+
+
+
+
+ sometimes i am also a quox. or three, depending on how you count.
+
+
+
+4. *bidirectional type checking* [@bidi] `*this one too*`
+5. crude-but-effective stratification [@crude; @crude-blog] for dealing with universes. `*does this need more detail too?*`
+6. *written in idris2*. that doesnโt really have much impact on the language itself, other than the compilation process, but iโm enjoying using a dependently typed language for something substantial. even if itโs one youโre not currently supposed to be using for anything substantial. also currently it spits out scheme, like idris, because that was easy.
+7. all the non-ascii syntax is [optional], but i like it.
+
+[optional]: https://git.rhiannon.website/rhi/quox/wiki/ascii-syntax
+
+as for what it _doesnโt_ have: any but the most basic of conveniences. sorry.
+
+
+
+# dependent types
+
+there are lots of languages with dependent typesโwell, quite a fewโso i wonโt spend too much time on this.
+
+`*but still something*`
+
+
+# closed type universe
+
+instead of having datatypes like in normal languages, in quox you get the basic building blocks to make them. the main building blocks are functions, pairs, enumerations, equality types, strings, and natural numbers. some sort of syntactic sugar to expand a datatype declaration into this representation _is_ something i want to add, but it'd be in the pretty distant future.
+
+:::aside
+_at the moment_, natural numbers are the only recursion possible. so you can define types with the same recursive structure, like lists, but binary trees and stuff are not _currently_ possible, until i replace them with something more general. probably w-types [@nlab-wtype].
+:::
+
+but right now you can define a few types like this. see [qtt](#qtt) below for what all the `0`s and `ฯ`s mean. due to the lack of generic recursion, but the presence of _natural numbers_ specifically, a list is a length, followed by a nested tuple of that length (terminated by `'nil`).
+
+```quox
+def0 Vec : โ โ โ โ โ =
+ ฮป n A โ
+ case n return โ of {
+ zero โ {nil};
+ succ p, As โ A ร As
+ } -- โ As = Vec p A
+
+def0 List : โ โ โ = ฮป A โ (n : โ) ร Vec n A
+
+def Nil : 0.(A : โ ) โ List A = ฮป A โ (0, 'nil)
+def Cons : 0.(A : โ ) โ A โ List A โ List A =
+ ฮป A x xs โ case xs return List A of { (len, xs) โ (succ len, x, xs) }
+
+def NilS = Nil String
+def ConsS = Cons String
+
+def example = ConsS "im" (ConsS "gay" NilS)
+
+def0 example-eq : example โก (2, "im", "gay", 'nil) : List String =
+ refl (List String) example
+```
+
+you might have noticed that i didn't write the eliminator. that is because they are kind of ugly. if you want to see it anyway you can find it in [the example folder][ex].
+
+[ex]: https://git.rhiannon.website/rhi/quox/src/commit/246d80eea2/examples/list.quox#L12-L25
+
+
+# qtt
+
+sometimes, values of some type can only be used in certain ways to make sense. this is hardly controversial; if you do this with
+
+
+a problem that dependent types used to have a lot is that the blurring of compile-time and run-time data can lead to more being retained than necessary.
+
+`*is there an example that has superlinear junk data without resorting to peano naturals or some shit*`
+
+consider this vector (length-indexed list) definition from a _hypothetical language_ with normal inductive types.
+
+```agda
+data Vect (A : โ ) : โ โ โ where
+ [] : Vect A 0
+ _โท_ : (n : โ) โ A โ Vect A n โ Vect A (succ n)
+```
+
+in a totally naive implementation, `cons` would store `n`, the length of its tail (and maybe even some kind of representation of `A` too). so a three element list would look something like
+
+
+# xtt
+
+`*mention about type-case and the closed universe*`
+
+
+# bidirectional type checking
+
+
+# references {#refs}
diff --git a/posts-wip/quox-type-system.md b/posts-wip/quox-type-system.md
new file mode 100644
index 0000000..7ea3d6c
--- /dev/null
+++ b/posts-wip/quox-type-system.md
@@ -0,0 +1,513 @@
+---
+title: quox's type system
+tags: [quox, programming]
+date: 2021-07-26
+...
+
+main inspirations:
+
+- [quantitative type theory](https://bentnib.org/quantitative-type-theory.pdf)
+ (2018\)
+ - mostly [conor's version](
+ https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf),
+ even though it's older (2016)
+ - track how often things are used in terms. you get linearity if you want
+ it, but also, predictable erasure
+- [graded modal dependent type theory](https://arxiv.org/pdf/2010.13163) (2021)
+ - a refinement of qtt. track occurrences in types too! your context becomes
+ two-dimensional but that's ok
+ - also the way quantities are tracked is a bit different
+- [observational type theory](
+ https://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf) (2007)
+ - nice middle ground between intensional and extensional type theory. you
+ get stuff like funext in a decidable setting
+- [xtt](https://arxiv.org/pdf/1904.08562.pdf)
+ ("extensional" type theory, but not that one) (2019)
+ - a cubical reformulation of the ideas in ott. no univalence stuff tho,
+ don't worry i'm still #UIPCrew
+
+
+
+the basic idea is to mash all of these things together, obviously, but also to
+embrace a closed type theory, so that stuff like the type-case in xtt can make
+sense, and try to be a nice language anyway. what's a datatype?
+
+the core then only needs to know about basic type formers like functions,
+pairs, w-types (:cold_sweat:), cubes (:cold_sweat:ย :cold_sweat:ย :cold_sweat:),
+etc, and their eliminators, instead of having to do the whole thing with
+datatypes and functions. those would still exist in an eventual surface
+language tho, since otherwise writing anything will be extremely painful, but
+elaborated to this stuff.
+
+
+# syntax
+
+:::defs
+$$
+\newcommand\EQ{\mathrel\Coloneqq}
+\newcommand\OR[1][]{\mkern17mu #1| \mkern10mu}
+\newcommand\Or{\mathrel|}
+\newcommand\KW\mathsf
+\newcommand\L\mathbfsf
+$$
+
+$$
+\newcommand\Type[1]{\KW{type}_{#1}}
+\newcommand\Tup[1]{\langle #1 \rangle}
+\newcommand\WTy{\mathbin\blacktriangleleft}
+\newcommand\WTm{\mathbin\vartriangleleft}
+\newcommand\BoxType{\mathop\blacksquare}
+\newcommand\BoxTy[1]{\mathop{\blacksquare_{#1}}}
+\newcommand\BoxTm{\mathop\square}
+\newcommand\Case{\KW{case}\:}
+\newcommand\Of{\:\KW{of}\:}
+\newcommand\Return{\:\KW{return}\:}
+\newcommand\Rec{\KW{rec}\:}
+\newcommand\With{\:\KW{with}\:}
+\newcommand\Arr{\mathrel\mapsto}
+\newcommand\TCArr{\mkern-10mu \Arr}
+\newcommand\Coe{\KW{coe}\:}
+\newcommand\Comp{\KW{comp}\:}
+\newcommand\Qty{\mathrel\diamond}
+$$
+:::
+
+bidirectional syntax. i like it.
+
+$$
+\begin{align*}
+x,y,z,X,Y,Z &\EQ \dotsb & \text{term variables} \\
+\iota &\EQ \dotsb & \text{dimension variables} \\
+\ell &\EQ n & \text{universe levels ($n \in \mathbb{N}$)} \\
+\L{a},\L{b},\L{c}, \text{etc} &\EQ \dotsb & \text{symbols} \\[.75em]
+%
+\pi,\rho,\phi,\sigma &\EQ 0 \Or 1 \Or \omega
+ & \text{quantities} \\[.75em]
+%
+q,r &\EQ \varepsilon \Or \iota & \text{dimensions} \\
+\varepsilon &\EQ 0 \Or 1 & \text{dimension endpoints} \\[.75em]
+%
+s,t,A,B &\EQ \Type\ell & \text{types \& terms: universe} \\
+ &\OR (x \Qty \pi,\rho : A) \to B \Or \lambda x. t
+ & \text{functions} \\
+ &\OR (x \Qty \rho : A) \times B \Or \Tup{s, t}
+ & \text{pairs} \\
+ &\OR (x \Qty \rho,\phi : A) \WTy B \Or s \WTm t
+ & \text{inductive data} \\
+ &\OR \{ \overline{\L{a}_i}^i \} \Or \L{a}
+ & \text{enumerations} \\
+ &\OR \BoxTy\pi A \Or \BoxTm s
+ & \text{quantity} \\
+ &\OR s =_{\iota.A} t \Or \lambda\iota.s
+ & \text{equalities} \\
+ &\OR \underline{e}
+ & \text{elimination in term} \\[.75em]
+%
+e, f &\EQ x & \text{eliminations: variable} \\
+ &\OR f \: s
+ & \text{application} \\
+ &\OR \Case e \Return z. A \Of \Tup{x, y} \Arr s
+ & \text{unpairing} \\
+ &\OR \Rec e \Return z. A \With s
+ & \text{recursion} \\
+ &\OR \Case e \Return z. A \Of
+ \{ \overline{\L{a}_i \Arr s_i}^i \}
+ & \text{enumeration} \\
+ &\OR \Case e \Return z. A \Of \BoxTm x \Arr s
+ & \text{quantity} \\
+ &\OR f \: q
+ & \text{equality application} \\
+ &\OR \Coe (\iota.A)^q_{q'} \: s
+ & \text{coercion} \\
+ &\OR[\left] \Comp A^q_{q'} \: s \:
+ \left\{
+ \begin{aligned}
+ (r=0) & \Arr \iota.t_0 \\
+ (r=1) & \Arr \iota.t_1
+ \end{aligned}
+ \right\} \right.
+ & \text{composition} \\
+ &\OR[\left] \Case e \Return A \Of
+ \left\{
+ \begin{array}{ll}
+ \Type{} & \TCArr t_0 \\
+ \Pi \: X \: Y & \TCArr t_1 \\
+ \Sigma \: X \: Y & \TCArr t_2 \\
+ \KW{W} \: X \: Y & \TCArr t_3 \\
+ \KW{Enum} & \TCArr t_4 \\
+ \BoxType X & \TCArr t_5 \\
+ \KW{Eq} \: X \: X' \: y \: z \: z' & \TCArr t_6 \\
+ \end{array}
+ \right\} \right.
+ & \text{type case} \\
+ &\OR s : A
+ & \text{annotation}
+\end{align*}
+$$
+
+__TODO wtf does all this cube stuff even mean. especially composition__
+
+i'm going to use abbreviations like $A \to_\pi B$ for $(x \Qty \pi,0 : A) \to
+B$, just $A$ for $z. A$ or $\iota. A$ in elim return types, etc for
+non-dependent stuff. $\emptyset$ means $\{\,\}$.
+
+a function type has two quantities attached to it, since unlike in qtt classique
+we care about what's going on in types too. in $(x \Qty \pi,\rho : A) \to B$,
+$x$ is used $\pi$ times in the body of a function of this type, and it's used
+$\rho$ times in $B$ itself.
+
+pairs $(x \Qty \rho : A) \times B$ only have one since it's just two things, the
+first doesn't occur in the second at all, but we still care about what's going
+on in $B$
+
+w-types $(x \Qty \rho,\phi : A) \WTy B$ also have two quantities, but in
+a different way. the $\rho$ still says how $x$ is used in $B$, but this time
+$\phi$ says how $x$ is used in $t$ in a term like $s \WTm \lambda x. t$.
+
+
+## examples of encodings
+
+also possible syntax. TODO universe & quantity polymorphism obviously
+
+```
+-- empty type
+Void : type 0 := {};
+
+absurd : (A @ 0,1 : type 0) -> Void @ 1 -> A :=
+ fun A v => case v return A of {};
+
+
+-- unit type
+Unit : type 0 := {'tt};
+
+swallow : (A @ 0,2 : type 0) -> Unit @ 1 -> A -> A :=
+ fun t x => case t return A of {'tt => x};
+
+
+-- boolean type
+Bool : type 0 := {'false; 'true};
+
+-- use 'case' for 'if'
+not : Bool @ 1 -> Bool :=
+ fun b => case b return Bool of {'false => 'true; 'true => 'false};
+
+
+-- natural numbers
+NatTag : type 0 := {'zero; 'suc};
+NatBody : NatTag @ 1 -> type 0 :=
+ fun n => case n return type 0 of {'zero => Void; 'suc => Unit};
+
+Nat : type 0 := (tag : NatTag @ 1,1) <|| NatBody tag;
+
+zero : Nat := 'zero <| absurd;
+suc : Nat @ 1 -> Nat := fun n => 'suc <| fun t => swallow t n;
+
+elimNat : (P @ inf,0 : Nat @ inf -> type 0) ->
+ (Z @ inf,0 : P zero) ->
+ (S @ inf,0 : (n @ 1,2 : Nat) -> P n -> P (suc n)) ->
+ (n @ inf,1 : Nat) -> P n :=
+ fun P Z S n =>
+ rec n return nโ. P nโ with fun tag =>
+ case tag
+ return t. (f @ inf,2 : NatBody t @ 0 -> Nat) ->
+ (IH @ inf,0 : (b @ 1 : NatBody t) -> P (f b)) ->
+ P (t <| f)
+ of {'zero => fun _ _ => Z;
+ 'suc => fun f IH => S (f 'tt) (IH 'tt)}
+```
+
+or something. :ghost: eliminators :ghost: w-types :ghost: \
+it's a core language and it's possible to translate a good language to
+these primitives, so try not to worry that it is impossible to write an
+elimination for a w-type correctly first try.
+
+btw, you can see in `elimNat` that the part after `with` is a partially applied
+function. this seems to be the most common pattern for dependent eliminators,
+which is why it's `rec n with s` instead of something like
+`case n of (tag <| f, IH) => s[tag,f,IH]`.
+getting rid of those `inf`s (and those in `elimNat`'s type) will need dependent
+quantities arrrg
+
+
+# type rules
+
+:::defs
+$$
+\newcommand\Q{\mathrel|}
+\newcommand\Z{\mathbf0}
+\newcommand\Chk{\mathrel\Leftarrow}
+\newcommand\Syn{\mathrel\Rightarrow}
+\newcommand\Ty[3]{\frac{\begin{matrix}#2\end{matrix}}{#3}\;\mathbfsf{#1}}
+\newcommand\AA{\textcolor{Purple}}
+\newcommand\BB{\textcolor{OliveGreen}}
+\newcommand\CC{\textcolor{RoyalBlue}}
+\newcommand\DD{\textcolor{Bittersweet}}
+\newcommand\EE{\textcolor{WildStrawberry}}
+\newcommand\FF{\textcolor{PineGreen}}
+\newcommand\GG{\textcolor{RedViolet}}
+\newcommand\HH{\textcolor{RedOrange}}
+$$
+:::
+
+:::rulebox
+$$
+\begin{gather}
+\Psi \Q \Delta \Q \Gamma \vdash
+ \AA{s} \Chk \BB{A}
+ \dashv \AA{\delta_s}; \BB{\delta_A} \\[.1em]
+\Psi \Q \Delta \Q \Gamma \vdash
+ \AA{e} \Syn \BB{A}
+ \dashv \AA{\delta_e}; \BB{\delta_A} \\
+\end{gather}
+$$
+:::
+
+ok. here we go. tybes. get ready for Density. to try and make things a little
+easier to pick out, quantities will be colour coded with where they came from.
+some of the colours are too similar. sorry.
+
+$$
+\begin{align*}
+\Gamma &\EQ \cdot \Or \Gamma, x : A
+ & \text{type context} \\
+\delta &\EQ \cdot \Or \delta, \pi x
+ & \text{quantity vector} \\
+\Delta &\EQ \cdot \Or \Delta, \delta
+ & \text{quantity context} \\
+\Psi &\EQ \cdot \Or \Psi, \iota \Or \Psi, q=r
+ & \text{cube}
+\end{align*}
+$$
+
+a context $\Gamma$ is a list of types, as always.
+
+a quantity context $\Delta$ is a triangle of how many times each type in
+$\Gamma$ uses all the previous ones. $\delta$ is a single vector of quantities,
+used for counting the quantities of everything in the subject and the subject's
+type. $0\Gamma$ means a quantity vector with the variables of $\Gamma$, with
+everything set to zero.
+
+a :ice_cube:ย cubeย :ice_cube: collects the dimension variables in scope, and
+constraints between them.
+
+the grtt paper (which doesn't have cubes) has this example (but written slightly
+differently):
+
+$$
+\left(\begin{smallmatrix}
+ \\
+ 1 A \\
+ 1 A & 0 x \\
+\end{smallmatrix}\right) \Q
+ (A: \Type0, x: A, y: A) \vdash
+ \AA{x} \Syn \BB{A}
+ \dashv \AA{(0A,1x,0y)}; \BB{(1A,0x,0y)}
+$$
+
+in $\Delta$ (the big thing at the beginning):
+
+- $A$ is the first element, so there is nothing it could mention, and it has
+ just an empty list $()$.
+- $x: A$ contains $A$ once, which is the only option, so it has $(1A)$.
+- $y: A$ also mentions $A$, but not $x$, so it's $(1A,0x)$.
+
+after the type of the subject are two more quantity vectors. the first is how
+the context elements are used in the subject itself, and the second how they're
+used in its type.
+
+by the way the reason i write the judgements this way with those two vectors at
+the end is because they are outputs, so now everything before $\vdash$ is an
+input, and everything after $\dashv$ is an output. whether the type is an input
+or output varies: since the syntax is bidirectional, $s \Chk A$ means that
+the term $s$ can only be checked against a known $A$ (so it's an input), and
+$e \Syn A$ means that for an elimination $e$ the type $A$ can be inferred (so
+it's an output).
+
+## universes
+
+$$
+\Ty{type}{
+ \AA{\ell} < \BB{\ell'}
+}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \AA{\Type\ell} \Chk \BB{\Type{\ell'}}
+ \dashv 0\Gamma; 0\Gamma
+}
+$$
+
+universes are cumulative. since we have a known universe to check against, why
+not.
+
+## functions
+
+$$
+\Ty{fun}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \AA{A} \Chk \Type\ell
+ \dashv \AA{\delta_A}; 0\Gamma \\
+ \Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
+ \BB{B} \Chk \Type\ell
+ \dashv (\BB{\delta_B}, \EE\rho x); (0\Gamma, 0x) \\
+}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ (x \Qty \DD\pi,\EE\rho : \AA{A}) \to \BB{B} \Chk \Type\ell
+ \dashv (\AA{\delta_A} + \BB{\delta_B}); 0\Gamma
+}
+$$
+
+in formation rules like this, the type-level quantities being all zero doesn't
+actually have to be checked, since everything is being checked against
+$\Type\ell$ which never uses variables. if universe polymorphism starts existing
+that will have to be tweaked in some way. maybe rules like __lam__ will have
+$\AA{\delta_A}; \FF{\delta_\ell}$ in the output of the first premise, and
+$\CC{\delta_t}; (\AA{\delta_A} + \BB{\delta_B} + \FF{\delta_\ell})$ in the
+conclusion. something like that.
+
+$$
+\Ty{lam}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \AA{A} \Chk \Type\ell
+ \dashv \AA{\delta_A}; 0\Gamma \\
+ \Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
+ \CC{t} \Chk \BB{B}
+ \dashv (\CC{\delta_t}; \DD\pi x); (\BB{\delta_B}; \EE\rho x) \\
+}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \lambda x. \CC{t} \Chk (x \Qty \DD\pi,\EE\rho : \AA{A}) \to \BB{B}
+ \dashv \CC{\delta_t}; (\AA{\delta_A} + \BB{\delta_B})
+}
+$$
+
+$$
+\Ty{app}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \FF{f} \Syn (x \Qty \DD\pi,\EE\rho : \AA{A}) \to \BB{B}
+ \dashv \FF{\delta_f}; (\AA{\delta_A} + \BB{\delta_B}) \\
+ \Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
+ \BB{B} \Chk \Type\ell
+ \dashv (\BB{\delta_B}, \EE\rho x); (0\Gamma, 0x) \\
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \CC{s} \Chk \AA{A}
+ \dashv \CC{\delta_s}; \AA{\delta_A} \\
+}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \FF{f} \: \CC{s} \Syn \BB{B}[\CC{s}/x]
+ \dashv (\FF{\delta_f} + \DD\pi\CC{\delta_s});
+ (\BB{\delta_B} + \EE\rho\CC{\delta_s})
+}
+$$
+
+the head of an application needs to inferrable, but a lambda isn't. so a
+ฮฒ redex is actually going to be something like
+$\big((\lambda x. t) : (x \Qty \pi,\rho : A) \to B\big) \: t$
+with an annotation on the head. probably from an inlined definition with a type
+signature.
+
+## pairs
+
+$$
+\Ty{pair}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \AA{A} \Chk \Type\ell
+ \dashv \AA{\delta_A}; 0\Gamma \\
+ \Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
+ \BB{B} \Chk \Type\ell
+ \dashv (\BB{\delta_B}, \EE\rho x); 0\Gamma \\
+}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ (x \Qty \EE\rho : \AA{A}) \times \BB{B} \Chk \Type\ell
+ \dashv (\AA{\delta_A} + \BB{\delta_B}); 0\Gamma
+}
+$$
+
+$$
+\Ty{comma}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \CC{s} \Chk \AA{A}
+ \dashv \CC{\delta_s}; \AA{\delta_A} \\
+ \Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
+ \BB{B} \Chk \Type\ell
+ \dashv (\BB{\delta_B}, \EE\rho x); 0\Gamma \\
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \DD{t} \Chk \BB{B}[\CC{s}/x]
+ \dashv \DD{\delta_t}; (\BB{\delta_B} + \EE\rho\CC{\delta_s}) \\
+}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \Tup{\CC{s}, \DD{t}} \Chk (x \Qty \EE\rho : \AA{A}) \times \BB{B}
+ \dashv (\CC{\delta_s} + \DD{\delta_t}); (\AA{\delta_A} + \BB{\delta_B})
+}
+$$
+
+$$
+\Ty{casepair}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \FF{e} \Syn (x \Qty \EE\rho : \AA{A}) \times \BB{B}
+ \dashv \FF{\delta_e}; (\AA{\delta_A} + \BB{\delta_B}) \\
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \AA{A} \Chk \Type\ell
+ \dashv \AA{\delta_A}; 0\Gamma \\
+ \Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
+ \BB{B} \Chk \Type\ell
+ \dashv (\BB{\delta_B}, \EE\rho x); 0\Gamma \\
+ \Psi \Q (\Delta, \AA{\delta_A} + \BB{\delta_B})
+ \Q (\Gamma, z: (x \Qty \EE\rho : \AA{A}) \times \BB{B}) \vdash
+ \GG{C} \Chk \Type\ell
+ \dashv (\GG{\delta_C}, \HH\sigma z); 0\Gamma \\
+ \Psi \Q (\Delta, \AA{\delta_A}, (\BB{\delta_B}, \EE\rho))
+ \Q (\Gamma, x : \AA{A}, y : \BB{B}) \vdash
+ \CC{s} \Chk \GG{C}[\Tup{x, y}/z]
+ \dashv (\CC{\delta_s}, \DD\pi x, \DD\pi y);
+ (\GG{\delta_C}, \HH\sigma x, \HH\sigma y)
+}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ (\Case \FF{e} \Return z. \GG{C} \Of \Tup{x, y} \Arr \CC{s})
+ \Syn \GG{C}[\FF{e}/z]
+ \dashv (\CC{\delta_s} + \DD\pi\FF{\delta_e});
+ (\GG{\delta_C} + \HH\sigma\FF{\delta_e})
+}
+$$
+
+## inductive data
+
+:^)
+
+## enumerations
+
+$$
+\Ty{enum}{}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \{ \overline{\L{a}_i}^i \} \Chk \Type\ell
+ \dashv 0\Gamma; 0\Gamma
+}
+$$
+
+$$
+\Ty{symbol}{
+ \L{a} \in \overline{\L{a}_i}^i
+}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \L{a} \Chk \{ \overline{\L{a}_i}^i \}
+ \dashv 0\Gamma; 0\Gamma
+}
+$$
+
+$$
+\Ty{caseenum}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \FF{e} \Syn \{\L{a}_i\}
+ \dashv \FF{\delta_e}; 0\Gamma \qquad
+ \overline{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \CC{s_i} \Chk \AA{A}[\L{a}_i/z]
+ \dashv \CC{\delta_s}; \AA{\delta_A}
+ }^i
+}{
+ \Psi \Q \Delta \Q \Gamma \vdash
+ \Case \FF{e} \Return z. \AA{A} \Of \{ \overline{\L{a}_i \Arr \CC{s_i}}^i \}
+ \dashv (\FF{\delta_e} + \CC{\delta_s}); \AA{\delta_A}
+}
+$$
+
+
+__TODO__ the rest
diff --git a/posts/2022-09-16-ats.md b/posts/ats.md
similarity index 100%
rename from posts/2022-09-16-ats.md
rename to posts/ats.md
diff --git a/posts/2022-07-12-beluga.md b/posts/beluga.md
similarity index 100%
rename from posts/2022-07-12-beluga.md
rename to posts/beluga.md
diff --git a/posts/chrismas.md b/posts/chrismas.md
new file mode 100644
index 0000000..53b6150
--- /dev/null
+++ b/posts/chrismas.md
@@ -0,0 +1,100 @@
+---
+date: 2023-12-25
+title: merr chrismas
+tags: [lรกntas, conlangs]
+conlang: laantas
+...
+
+# just tell me how to say it please
+
+sure thing. here.
+
+:::glosses
+- ufit รพulkusimsari
+- [หufit หฮธuษซkษsiฬsษสi]
+- ufi-t รพulkusi-m-sa-ri
+- cozy-GEN midwinter-DEF-AD-PRL
+- (be) cozy during midwinter
+:::
+
+
+# details
+
+now i am not a huge fan of putting christianity into my conlang, which is
+hopefully understandable. but having a midwinter festival sounds cute. the days
+are finally getting longer! you made it through the worst part! and so on. so
+that's what this is. i think it probably takes place the day after the solstice,
+but with several days of festivities, so that there is still a little overlap
+with the _other_ winter holiday. it's still appropriate to say it today.
+
+## seasons
+
+| time | name | | pron. | translation |
+|----------|---------------|--------------|--------------|-------------|
+| nov--jan | `{#igisim}` | `{igisim}` | `[หiสษsiฬ]` | the freeze |
+| feb | `{#susurum}` | `{susurum}` | `[หsusสroฬ]` | the melt |
+| mar--may | `{#ลกangubam}` | `{ลกangubam}` | `[หสaลษกษvษฬ]` | the bloom |
+| jun--aug | `{#guwanแธฟ}` | `{guwanแธฟ}` | `[หษกษwษnmฬฉ]` | the sun |
+| sep--oct | `{#santum}` | `{santum}` | `[หsantoฬ]` | the rain |
+
+- in between `{!igisim}` (winter) and `{!ลกangubam}` (spring), the month of
+ february is considered a transition between the two, `{!susurum}`.
+- as a result, `{!santum}` (autumn) is only two months long.
+- `{!ลกangubam}` comes from `{!ลกani}` (flower) and `{!guba}` (grow, thrive).
+
+## putting it together
+
+the word "midwinter", without any inflections, is `{!รพulkusim}`, which comes
+from `{!รพulku}` "be deep" and `{!igisim}`. unusually for lรกntas, `{!รพulku}` is a
+verb, rather than a noun. why? who knows.
+
+::: {.aside .floating}
+on that page, where you see a `{ฦถ}`, replace it with `{รพ}`. i haven't got round
+to updating that yet. it also has the ugly text until i redraw `{!ฤ\ วง\}`, since
+at least if it's all ugly it's consistent. sorry about that.
+:::
+
+the suffix `{!โsari}` is actually a pair of two suffixes, which together mean
+through, or during. the details of the whole situation are [here][loc], but it
+is a cool two-dimensional system based on a thing that can be found in some
+languages of the caucasus. the `{!โm}` on the end (of all these words so far,
+actually) is "the". so the full form `{!รพulkusimsari}` means "during midwinter".
+
+now, for `{!ufit}`. there is a small, but technically non-zero, chance that you
+remember the word `{!uf{a}t}` from [here][hallow], with the meaning of "warm".
+this is actually the same word, but a bit cutesy. so, cozy.
+
+the implied verb in this sentence is `{!iksaha}`, like before. this is an
+auxiliary verb for requests. for example, if `{!ลกikkรบha}` means "you are going",
+then `{!ลกikkรบm iksaha}` means "please go away". the `{โha}` here means "you"
+(singular). here it's dropped because the phrase is long enough already to be
+easily understood.
+
+so in the end, you get `{!ufit รพulkusimsari}`, meaning "[stay] cozy during the
+midwinter".
+
+
+:::twocol-grid
+{width=100%}
+
+::: {.glosses .left}
+- รพugusim ai
+- [หฮธuษฃษsiฬmโฟai]
+- รพugusi-m ai
+- miwiner-DEF be
+- it crismas
+:::
+
+{width=100%}
+
+::: {.glosses .left}
+- ufi รพugusinhari
+- [หufi หฮธuษฃษsiฬลxษสi]
+- ufi-(t) รพugusi-m-hari
+- cozy-(GEN) miwiner-DEF-DURINโ
+- merr crismas
+:::
+:::
+
+[loc]: https://lang.niss.website/laantas/nouns.html#locational-cases
+[hallow]: https://cohost.org/niss/post/3366713-ufat-iksaha
diff --git a/posts/2022-03-14-digitle-in-maude.md b/posts/digitle-in-maude.md
similarity index 100%
rename from posts/2022-03-14-digitle-in-maude.md
rename to posts/digitle-in-maude.md
diff --git a/posts/2022-10-24-fib.md b/posts/fib.md
similarity index 100%
rename from posts/2022-10-24-fib.md
rename to posts/fib.md
diff --git a/posts/2022-11-12-idris2-features.md b/posts/idris2-features.md
similarity index 100%
rename from posts/2022-11-12-idris2-features.md
rename to posts/idris2-features.md
diff --git a/quox.bib b/quox.bib
new file mode 100644
index 0000000..4243153
--- /dev/null
+++ b/quox.bib
@@ -0,0 +1,182 @@
+% quantitative stuff
+
+@inproceedings{grtt,
+ author = {Moon, Benjamin and Eades, III, Harley and Orchard, Dominic},
+ editor = {Yoshida, Nobuko},
+ title = {Graded Modal Dependent Type Theory},
+ booktitle = {Programming Languages and Systems:
+ European Symposium on Programming ({ESOP})},
+ series = {Lecture Notes in Computer Science},
+ volume = {12648},
+ pages = {462--490},
+ publisher = {Springer},
+ year = {2021},
+ url = {https://doi.org/10.1007/978-3-030-72019-3\_17},
+ doi = {10.1007/978-3-030-72019-3\_17}
+}
+
+@inproceedings{nuttin,
+ author = {Conor McBride},
+ editor = {Sam Lindley and Conor McBride and
+ Philip W. Trinder and Donald Sannella},
+ title = {I Got Plenty o' Nuttin'},
+ booktitle = {A List of Successes That Can Change the World---Essays Dedicated
+ to {P}hilip {W}adler on the Occasion of His 60th Birthday},
+ pages = {207--233},
+ publisher = {Springer},
+ year = {2016},
+% url = {https://doi.org/10.1007/978-3-319-30936-1\_12},
+ url = {https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf},
+}
+
+@inproceedings{qtt,
+ author = {Robert Atkey},
+ editor = {Anuj Dawar and
+ Erich Grรคdel},
+ title = {Syntax and Semantics of Quantitative Type Theory},
+ booktitle = {Logic in Computer Science ({LICS})},
+ pages = {56--65},
+ publisher = {{ACM}},
+ year = {2018},
+% url = {https://doi.org/10.1145/3209108.3209189},
+ url = {https://bentnib.org/quantitative-type-theory.pdf}
+}
+
+
+% observational stuff
+
+@inproceedings{ott-now,
+ author = {Thorsten Altenkirch and Conor McBride and Wouter Swierstra},
+ editor = {Aaron Stump and Hongwei Xi},
+ title = {Observational equality, now!},
+ booktitle = {Programming Languages meets Program Verification ({PLPV})},
+ publisher = {{ACM}},
+ year = {2007},
+ url = {https://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf},
+}
+
+@inproceedings{ott-good,
+ author = {Loรฏc Pujet and Nicolas Tabareau},
+ title = {Observational equality: now for good},
+ booktitle = {Principles of Programming Languages ({POPL})},
+ pages = {1--27},
+ year = {2022},
+ url = {https://doi.org/10.1145/3498693},
+ doi = {10.1145/3498693},
+}
+
+@inproceedings{xtt,
+ author = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
+ editor = {Herman Geuvers},
+ title = {Cubical Syntax for Reflection-Free Extensional Equality},
+ booktitle = {Formal Structures for Computation and Deduction ({FSCD})},
+ series = {LIPIcs},
+ volume = {131},
+ pages = {31:1--31:25},
+ publisher = {Schloss Dagstuhl - Leibniz-Zentrum fรผr Informatik},
+ year = {2019},
+% url = {https://doi.org/10.4230/LIPIcs.FSCD.2019.31},
+ url = {https://arxiv.org/pdf/1904.08562.pdf},
+ doi = {10.4230/LIPIcs.FSCD.2019.31}
+}
+
+
+% Misc type stuff
+
+@misc{crude,
+ author = {McBride, Conor},
+ title = {Crude but effective stratification (slides)},
+ url = {https://personal.cis.strath.ac.uk/conor.mcbride/Crude.pdf},
+ note = {Slides}
+}
+
+@misc{crude-blog,
+ author = {McBride, Conor},
+ title = {Crude but Effective Stratification},
+ url = {https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html},
+ year = {2011},
+}
+
+@inproceedings{mugen,
+ author = {Hou (Favonia), Kuen-Bang and Angiuli, Carlo and Mullanix, Reed},
+ title = {An Order-Theoretic Analysis of Universe Polymorphism},
+ month = {jan},
+ year = {2023},
+ url = {https://doi.org/10.1145/3571250},
+ doi = {10.1145/3571250},
+ booktitle = {Principles of Programming Languages ({POPL})},
+}
+
+@article{bidi,
+ author = {Jana Dunfield and Neel Krishnaswami},
+ title = {Bidirectional Typing},
+ journal = {{ACM} Computing Surveys},
+ volume = {54},
+ number = {5},
+ year = {2022},
+ url = {https://doi.org/10.1145/3450952},
+ doi = {10.1145/3450952},
+}
+
+
+% Misc implementation
+
+@article{expl-sub,
+ author = {Martรญn Abadi and Luca Cardelli and
+ Pierre{-}Louis Curien and Jean{-}Jacques Lรฉvy},
+ title = {Explicit Substitutions},
+ journal = {Journal of Functional Programming},
+ volume = {1},
+ number = {4},
+ pages = {375--416},
+ year = {1991},
+ url = {http://lucacardelli.name/Papers/ExplicitSub.pdf}
+}
+
+% historical
+
+@inproceedings{indices,
+ author = {Edwin C. Brady and Conor McBride and James McKinna},
+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
+ title = {Inductive Families Need Not Store Their Indices},
+ booktitle = {Types for Proofs and Programs ({TYPES})},
+ series = {Lecture Notes in Computer Science},
+ volume = {3085},
+ pages = {115--129},
+ publisher = {Springer},
+ year = {2003},
+ url = {https://doi.org/10.1007/978-3-540-24849-1\_8},
+ doi = {10.1007/978-3-540-24849-1\_8},
+ note = {\textit{i couldn't find a non-paywalled version, sorry!
+ but it's mostly for historical interest anyway}}
+}
+
+% blog post specific
+@misc{nlab-wtype,
+ author = {{nLab authors}},
+ title = {{W}-type},
+ howpublished = {\url{https://ncatlab.org/nlab/show/W-type}},
+ note = {\href{https://ncatlab.org/nlab/revision/W-type/47}{revision 47}},
+ month = nov,
+ year = 2023
+}
+
+@book{martinlof84,
+ author = {Per Martin-Lรถf},
+ title = {Intuitionistic type theory},
+ series = {Studies in proof theory},
+ volume = {1},
+ publisher = {Bibliopolis},
+ year = {1984},
+ isbn = {978-88-7088-228-5},
+ url = {https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf}
+}
+
+% bullshit
+
+@misc{hotminute,
+ author = {{Wiktionary}},
+ title = {Hot minute},
+ year = {2023},
+ url = {https://en.wiktionary.org/wiki/hot_minute},
+}
diff --git a/style/counters.css b/style/counters.css
index 8dfb591..5e8d356 100644
--- a/style/counters.css
+++ b/style/counters.css
@@ -2,63 +2,45 @@
--section-prefix: '';
}
-h1::before, h2::before, h3::before, h4::before, h5::before, h6::before {
+main :is(h1, h2, h3, h4, h5, h6):not(.unnumbered)::before {
padding-right: 1ex;
}
-main h1 {
- counter-increment: h1;
- counter-reset: h2 h3 h4 h5 h6;
-}
-
-main h1::before {
+main h1:not(.unnumbered) { counter-increment: h1; }
+main h1 { counter-reset: h2 h3 h4 h5 h6; }
+main h1:not(.unnumbered)::before {
content: var(--section-prefix) counter(h1);
}
-main h2 {
- counter-increment: h2;
- counter-reset: h3 h4 h5 h6;
-}
-
-main h2::before {
+main h2:not(.unnumbered) { counter-increment: h2; }
+main h2:not(.unnumbered)::before {
content: var(--section-prefix) counter(h1) '.' counter(h2);
}
+main h2 { counter-reset: h3 h4 h5 h6; }
-main h3 {
- counter-increment: h3;
- counter-reset: h4 h5 h6;
-}
-
-main h3::before {
+main h3:not(.unnumbered) { counter-increment: h3; }
+main h3 { counter-reset: h4 h5 h6; }
+main h3:not(.unnumbered)::before {
content: var(--section-prefix) counter(h1) '.' counter(h2) '.' counter(h3);
}
-main h4 {
- counter-increment: h4;
- counter-reset: h5 h6;
-}
-
-main h4::before {
+main h4:not(.unnumbered) { counter-increment: h4; }
+main h4 { counter-reset: h5 h6; }
+main h4:not(.unnumbered)::before {
content: var(--section-prefix)
counter(h1) '.' counter(h2) '.' counter(h3) '.' counter(h4);
}
-main h5 {
- counter-increment: h5;
- counter-reset: h6;
-}
-
-main h5::before {
+main h5:not(.unnumbered) { counter-increment: h5; }
+main h5 { counter-reset: h6; }
+main h5:not(.unnumbered)::before {
content: var(--section-prefix)
counter(h1) '.' counter(h2) '.' counter(h3) '.' counter(h4) '.'
counter(h5);
}
-main h6 {
- counter-increment: h6;
-}
-
-main h6::before {
+main h6:not(.unnumbered) { counter-increment: h6; }
+main h6:not(.unnumbered)::before {
content: var(--section-prefix)
counter(h1) '.' counter(h2) '.' counter(h3) '.' counter(h4) '.'
counter(h5) '.' counter(h6);
diff --git a/style/niss.png b/style/niss.png
new file mode 100644
index 0000000..0e2009e
Binary files /dev/null and b/style/niss.png differ
diff --git a/style/page.css b/style/page.css
index a88d634..9d53405 100644
--- a/style/page.css
+++ b/style/page.css
@@ -1,3 +1,4 @@
+@import url(fonts/schola/schola.css);
@import url(fonts/muller/muller.css);
@import url(fonts/junius/junius.css);
@import url(fonts/pragmatapro/pragmatapro.css);
@@ -14,7 +15,7 @@
:root {
background: var(--root-col);
- font-family: Muller;
+ font-family: schola;
font-size: 16pt;
height: 100vh;
@@ -46,36 +47,38 @@ header h1 {
h1, h2, h3, h4, h5, h6 {
margin: 1em 0 0.25em;
+ font-family: Muller;
+ clear: both;
}
h1 {
- font-size: 200%;
- font-weight: 200;
-}
-
-h2 {
- font-size: 180%;
- font-weight: 200;
-}
-
-h3 {
- font-size: 160%;
+ font-size: 150%;
font-weight: 300;
}
-h4 {
+h2 {
font-size: 140%;
font-weight: 300;
}
-h5 {
+h3 {
+ font-size: 130%;
+ font-weight: 300;
+}
+
+h4 {
font-size: 120%;
+ font-weight: 300;
+}
+
+h5 {
+ font-size: 110%;
font-weight: 400;
}
h6 {
font-size: 100%;
- font-weight: 400;
+ font-weight: 600;
}
header h1 {
@@ -142,6 +145,11 @@ b, strong {
font-weight: 600;
}
+dfn {
+ font-style: normal;
+ font-weight: 500;
+}
+
ul li {
list-style: 'โ ';
}
@@ -172,6 +180,7 @@ code {
}
pre {
+ clear: both;
width: min-content;
margin: 0.5em auto;
padding: 0.5em 0.8em;
@@ -200,9 +209,9 @@ pre {
font-weight: 700;
}
-.abbr {
+.gloss .abbr {
font-size: 70%;
- font-weight: 500;
+ font-weight: bold;
}
.scr {
@@ -308,6 +317,15 @@ figure li {
break-inside: avoid;
}
+figcaption {
+ font-size: 80%;
+ font-style: italic;
+ margin: auto;
+}
+:not(.floating) > figcaption {
+ width: 75%;
+}
+
dt { font-weight: 500; float: left; clear: left; }
dd { margin-left: 4em; }
@@ -336,7 +354,19 @@ u u {
margin-top: 0;
}
+.twocol-grid {
+ display: grid;
+ grid-template-columns: 1fr 1fr;
+ gap: 1em;
+ margin: 1em 0;
+}
+
+.twocol-grid .gloss {
+ margin-left: 0;
+}
+
footer {
+ clear: both;
margin: 1.5em auto 1em;
padding-top: 0.5em;
@@ -385,24 +415,133 @@ blockquote {
}
-aside {
+.note, aside {
font-size: 90%;
- margin: 0.5em 3em;
- border-left: 2px solid var(--root-col);
- padding-left: 1em;
}
+.note {
+ font-style: italic;
+}
+
+:is(h1, h2) .note {
+ font-size: 75%;
+}
+
+aside {
+ margin: 0.5em 3em;
+ padding-left: 1em;
+}
+aside:not(.no-line) {
+ border-left: 2px solid var(--root-col);
+}
+
+aside > details summary {
+ font-weight: 600;
+}
+
+aside :is(h1, h2, h3, h4, h5, h6) {
+ margin-top: 0.25em;
+ font-weight: 600;
+}
+aside h1 { font-size: 115%; }
+aside :is(h2, h3, h4, h5, h6) { font-size: 100%; }
+
+:is(aside, figure).floating {
+ max-width: 33%;
+}
+aside.floating {
+ padding: 0.25em 0.75em;
+ margin: 0.15em 1em 0;
+}
+figure.floating {
+ margin: 0 0.5em;
+}
+
+aside.floating :first-child { margin-top: 0; }
+aside.floating :last-child { margin-bottom: 0; }
.kw { color: hsl(300deg, 60%, 30%); }
.pp { color: hsl(343deg, 100%, 40%); /* font-weight: 500; */ }
.dt { color: hsl(173deg, 100%, 24%); /* font-weight: 500; */ }
-.fu { color: hsl(34deg, 100%, 30%); /* font-weight: 500; */ }
+.fu, .at { color: hsl(34deg, 100%, 30%); /* font-weight: 500; */ }
.va { color: hsl(203deg, 100%, 30%); /* font-weight: 500; */ }
.cf { color: hsl(276deg, 75%, 35%); /* font-weight: 500; */ }
.op { color: hsl(220deg, 40%, 33%); }
-.co { color: hsl(221deg, 10%, 39%); font-style: italic; }
+.co { color: hsl(221deg, 10%, 39%); /* font-style: italic; */ }
.bu { color: hsl(120deg, 85%, 25%); }
-:is(.st, .fl, .dv, .sc) { color: hsl(143deg, 100%, 20%); }
+.st, .fl, .dv, .bn, .sc, .ss { color: hsl(143deg, 100%, 20%); }
.wa { color: hsl(350deg, 80%, 25%); text-decoration: wavy 1.5px underline; }
.al { color: hsl(350deg, 80%, 25%); }
.cn { color: hsl(343deg, 100%, 30%); }
+
+
+.floating {
+ float: right;
+ margin: 0.5em 1em 0.5em 2em;
+}
+
+.floating.left {
+ float: left;
+ margin: 0.5em 2em 0.5em 1em;
+}
+
+.shaped {
+ /* maybe one day... */
+ /* shape-outside: attr(src url); */
+ shape-margin: 1em;
+}
+
+.shadow { filter: drop-shadow(5px 5px 8px #0006); }
+
+.pixel {
+ image-rendering: crisp-edges;
+ image-rendering: pixelated;
+}
+
+
+.citation {
+ font-size: 90%;
+}
+
+#refs {
+ margin-top: 0.75em;
+}
+.csl-entry {
+ margin-left: 2em;
+ text-indent: -2em;
+}
+/*
+.csl-entry {
+ display: grid;
+ grid-template-columns: 4ch auto;
+ grid-gap: 1ex;
+}
+.csl-left-margin {
+ justify-self: end;
+}
+*/
+
+.texdefs {
+ display: none;
+}
+
+.rulebox {
+ float: right;
+ border: 1px solid var(--root-col);
+ background: #ffffff66;
+ padding: .4em 1.2em;
+}
+
+/* the last thing in the :is is for priority fuckery */
+.rulebox :is(p, .math, mjx-container, #asd) {
+ margin: 0;
+ padding: 0;
+}
+
+.clear { clear: both; }
+
+mark {
+ mix-blend-mode: multiply;
+ background: #fbc;
+ padding: 0 0.35ch;
+}
diff --git a/syntax/quox.xml b/syntax/quox.xml
new file mode 100644
index 0000000..5f06be5
--- /dev/null
+++ b/syntax/quox.xml
@@ -0,0 +1,167 @@
+
+
+
+
+]>
+
+
+
+ load
+
+
+ String
+ IOState
+ โNat
+ Eq
+ Type
+
+
+
+ fstsnd
+ coecomp
+ ฮปfun
+ ฮดdfun
+ returnof
+ returnof
+ zerosucc
+
+
+
+ fail
+ main
+ compile-scheme
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/templates/post.html b/templates/post.html
index 4023132..e525826 100644
--- a/templates/post.html
+++ b/templates/post.html
@@ -25,7 +25,7 @@ $head()$
$if(show-toc)$
+ 
+ 
