diff --git a/.gitignore b/.gitignore
index d2a6a5a..4f19501 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
dist-newstyle
_build
_tmp
+.directory
+*~
diff --git a/images/bub_flop.png b/images/bub_flop.png
new file mode 100644
index 0000000..3af302d
Binary files /dev/null and b/images/bub_flop.png differ
diff --git a/images/crismas1.png b/images/crismas1.png
deleted file mode 100644
index e7b98cd..0000000
Binary files a/images/crismas1.png and /dev/null differ
diff --git a/images/crismas2.png b/images/crismas2.png
deleted file mode 100644
index 7097ee9..0000000
Binary files a/images/crismas2.png and /dev/null differ
diff --git a/images/panqt.nobg.png b/images/panqt.nobg.png
deleted file mode 100644
index ecdadf6..0000000
Binary files a/images/panqt.nobg.png and /dev/null differ
diff --git a/images/panqt.nobg2x.png b/images/panqt.nobg2x.png
deleted file mode 100644
index 7598716..0000000
Binary files a/images/panqt.nobg2x.png and /dev/null differ
diff --git a/images/panqt.png b/images/panqt.png
deleted file mode 100644
index 43e5080..0000000
Binary files a/images/panqt.png and /dev/null differ
diff --git a/images/panqt2x.png b/images/panqt2x.png
deleted file mode 100644
index 8e405cb..0000000
Binary files a/images/panqt2x.png and /dev/null differ
diff --git a/images/qt.svg b/images/qt.svg
deleted file mode 100644
index a7caf28..0000000
--- a/images/qt.svg
+++ /dev/null
@@ -1,128 +0,0 @@
-
-
-
\ No newline at end of file
diff --git a/images/quorientation.png b/images/quorientation.png
deleted file mode 100644
index 8af38fb..0000000
Binary files a/images/quorientation.png and /dev/null differ
diff --git a/images/quox-tod.png b/images/quox-tod.png
deleted file mode 100644
index b9edb50..0000000
Binary files a/images/quox-tod.png and /dev/null differ
diff --git a/images/quox.png b/images/quox.png
deleted file mode 100644
index 96bf9f4..0000000
Binary files a/images/quox.png and /dev/null differ
diff --git a/images/skip-some-floors.png b/images/skip-some-floors.png
deleted file mode 100644
index f5601dd..0000000
Binary files a/images/skip-some-floors.png and /dev/null differ
diff --git a/images/yummycricket.png b/images/yummycricket.png
deleted file mode 100644
index 2953d7b..0000000
Binary files a/images/yummycricket.png and /dev/null differ
diff --git a/posts-wip/2023-06-05-quox.md b/posts-wip/2023-06-05-quox.md
deleted file mode 100644
index 2e5a53b..0000000
--- a/posts-wip/2023-06-05-quox.md
+++ /dev/null
@@ -1,315 +0,0 @@
----
-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-10-25-quox.md b/posts-wip/2023-10-25-quox.md
deleted file mode 100644
index e792b2e..0000000
--- a/posts-wip/2023-10-25-quox.md
+++ /dev/null
@@ -1,112 +0,0 @@
----
-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/quox-type-system.md b/posts-wip/quox-type-system.md
deleted file mode 100644
index 7ea3d6c..0000000
--- a/posts-wip/quox-type-system.md
+++ /dev/null
@@ -1,513 +0,0 @@
----
-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-wip/rainbow-quox.md b/posts-wip/rainbow-quox.md
new file mode 100644
index 0000000..84186c4
--- /dev/null
+++ b/posts-wip/rainbow-quox.md
@@ -0,0 +1,274 @@
+---
+title: rainbow quox
+date: 2024-11-17
+tags: [computer, website, fursona]
+summary: q.t. colour scheme generator
+...
+
+so how about that regular posting, huh. ha ha ha
+
+i haven't been up to much unusual. [drawing], mostly. i installed [nixos] on both my computers and it's going pretty well so far [(less than a week)]{.note}, but every computer toucher does that at some point, so, whatever.
+
+[drawing]: https://gallery.niss.website
+[nixos]: https://nixos.org
+
+anyway, to the point.
+
+:::banner
+[go here if you just want to play with the thing][thing]
+
+:::
+
+# the point {.unnumbered}
+
+the animal-inclined might know that [q.t.][qt] can change its colour any time it wants. if you click that link you can clearly see i have some tendencies, but it can in theory be anything. so something i have wanted for a while is a page where you can click a button and get a bespoke randomly-generated quox theme of your very own.
+
+so i did that.
+
+:::aside
+you can also skip to [what i _actually_ ended up doing](#actual), if you don't care about the false starts.
+:::
+
+[qt]: https://gallery.niss.website/by-any/#qt
+
+# doing that
+
+{.floating .expandable .nobg .shaped}
+
+pretty much what i want to do, at least to begin with, is take the original colours of the image and move the hues around at random.
+
+if you look at [mdn], you might see this interesting [`hue-rotate()`][hr] thing that might do what i want. let's have a look.
+
+[mdn]: https://developer.mozilla.org/en-US/docs/Web/CSS
+[hr]: https://developer.mozilla.org/en-US/docs/Web/CSS/filter-function/hue-rotate
+
+> **Note:** `hue-rotate()` is specified as a matrix operation on the RGB color. It does not actually convert the color to the HSL model, which is a non-linear operation. Therefore, it may not preserve the saturation or lightness of the original color, especially for saturated colors.
+
+well that doesn't sound very promising. but maybe it'll be fine, so let's try it. first, separate the pictures from [q.t.'s refsheet][ref] into bits. like this.
+
+[ref]: https://gallery.niss.website/main/niss/2024-06-27-qt
+
+{.expandable .lightbg}
+
+now let's layer them back on top of each other with some css.
+
+```html
+
+
+
+
+
+
+
+
+```
+
+{.floating .left .nobg .expandable .shaped}
+
+ok, next, actually try to do the hue stuff. to check it works at all, i shoved everything to hue 0° (using krita's _hue HSL_ blend mode), and used `hue-rotate()` to change it back to the 'main' colour of each region---it won't look exact, but it'll be close.
+
+```css
+#container img { filter: hue-rotate(var(--hue)); }
+
+#outer { --hue: 273deg; } #belly { --hue: 26deg; }
+#eyes { --hue: 133deg; } #masks { --hue: 284deg; }
+#stripes { --hue: 188deg; } #lines { --hue: 273deg; }
+/* also add the id to each image */
+```
+
+right?
+
+{.expandable .nobg}
+
+well that's no good at all. i guess that warning was serious.
+
+# ok what about blend modes
+
+{.floating .expandable}
+
+all right, fine. what else. as a chronic over-user of `overlay`, i can certainly tell you that css has a few [blending modes][bm]. not as many as krita, which has approximately "too many", but enough for most purposes. one of them is `hue`. how about that.
+
+[bm]: https://developer.mozilla.org/en-US/docs/Web/CSS/blend-mode
+
+this takes a bit more messing, because i need to create a flood fill of one of the colours from that layer, and blend with that. so how about an SVG filter, i guess. or, six SVG filters---one for each filter, since you can't parametrise them.
+
+time to copy and paste the same five lines six times. yaaaaaaaaay
+
+{.bigemoji .pixel} \
+
+```svg
+
+```
+
+```css
+#outer { filter: url(#fouter); }
+/* …etc… */
+```
+
+and…
+
+{.expandable .nobg}
+
+i was expecting at least the same thing, but a different, also wrong, result is pretty cool.
+
+# drastic measures {#actual}
+
+ok, enough messing around, time to bite the bullet. separate every single colour into its own layer, and use those as _masks_ for colour fills.
+
+now the pieces look like _this_:
+
+{.expandable .lightbg}
+
+the colours in the images no longer matters, only the alpha channel. [(except for the eyes.)]{.note} each one is just a mask over a background fill of the right colour.
+
+```css
+@layer {
+ #container { position: relative; width: 90vw; aspect-ratio: 3439/2240; }
+ #container div { position: absolute; inset: 0; mask-size: contain; }
+}
+
+@layer {
+ #static { background: url(front/static.png) 0 0 / contain; }
+ #eye-shine {
+ background: url(front/eyes.png) 0 0 / contain;
+ mix-blend-mode: luminosity;
+ }
+ /* the others all look like this: */
+ #spines {
+ background: oklch(30.77% 0.1306 var(--hue)); --hue: 298.19;
+ mask-image: url(front/spines.png);
+ }
+ /* etc… */
+}
+```
+
+```html
+
+
+
+
+
+
+
+
+```
+
+since the hue is separated out into a variable, i can just do:
+
+```js
+for (const elem of document.getElementsByClassName('part')) {
+ elem.style.setProperty('--hue', Math.random() * 360);
+}
+```
+
+and instantly i have _something_ working. i used `oklch` because it was more likely than `hsl` or whatever to keep the colours the same kind of distance from each other, since that is what it's designed for.
+
+{.expandable .hasborder}
+
+
+# keeping the colours in sync
+
+so as of last year, most browsers got a thing called [relative colours]. if you have an existing colour `--hi`, you can rotate its hue by half a turn by saying something like
+
+[relative colours]: https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_colors/Relative_colors
+
+```css
+:root {
+ --hi: #ea9aa1;
+ --wow: oklch(from var(--hi) l c calc(h + 180));
+}
+```
+
+---
+header-includes: |
+
+...
+
+
+
\--hi
+
\--wow
+
+
+you're taking the value of `var(--hi)`, keeping the lightness and chroma channels the same, and adding 180° to the hue.
+
+:::aside
+that's not quite true. safari, as always, does it slightly wrong. according to the spec, all channels in a relative colour must be dimensionless, but in safari, the hue is an ``. other browsers, following the spec correctly, _don't allow_ that. so you _actually_ have to write
+
+```css
+:root {
+ --hi: #ea9aa1;
+ --wow: oklch(from var(--hi) l c calc(h + 180));
+}
+@supports (color: oklch(from red l c 10deg)) {
+ :root { --wow: oklch(from var(--hi) l c calc(h + 180deg)); }
+}
+```
+
+thanks apple!
+:::
+
+so based on that, i can pick one initial colour and base all the others on it. like
+
+```css
+:root {
+ /* these aren't attempting to be the same colours, just guessing something
+ that MIGHT look nice */
+ --outer: #57267e;
+ --spines: oklch(from var(--outer) calc(l * .75) calc(c * 1.25) h);
+ --vitiligo1: oklch(from var(--outer) calc(1 - (1 - l)/4) calc(c / 2) h);
+
+ /* static l/c values because the socks are always some pale colour */
+ --stripes: oklch(from var(--outer) .9 12.5% calc(h + 120));
+ --cuffs: oklch(from var(--stripes) .8 25% h);
+ /* etc */
+}
+
+.outer { background: var(--outer); mask-image: url(front/outer.png); }
+/* etc */
+```
+
+so after guessing a bunch of relative colours, i ended up with this:
+
+{.expandable .nobg}
+
+
+## notes for niss. if this goes online i fucked up
+
+- palette types
+- randomise distance between analogous colours
+- light, dark, light-dark, dark-light (belly vs outer)
+- reinstate chaos mode
+- can you set the random seed in the browser
+ - no. anyway the algorithm might be different
+ - make yr own
+ - or . whatever
+- if so: use that to make palette permalinks
diff --git a/posts-wip/rainbow-quox/blends.avif b/posts-wip/rainbow-quox/blends.avif
new file mode 100644
index 0000000..e6904bc
Binary files /dev/null and b/posts-wip/rainbow-quox/blends.avif differ
diff --git a/posts-wip/rainbow-quox/dark.avif b/posts-wip/rainbow-quox/dark.avif
new file mode 100644
index 0000000..c75851f
Binary files /dev/null and b/posts-wip/rainbow-quox/dark.avif differ
diff --git a/posts-wip/rainbow-quox/dark2.avif b/posts-wip/rainbow-quox/dark2.avif
new file mode 100644
index 0000000..58be28b
Binary files /dev/null and b/posts-wip/rainbow-quox/dark2.avif differ
diff --git a/posts-wip/rainbow-quox/front.avif b/posts-wip/rainbow-quox/front.avif
new file mode 100644
index 0000000..65bc2ba
Binary files /dev/null and b/posts-wip/rainbow-quox/front.avif differ
diff --git a/posts-wip/rainbow-quox/pieces1.avif b/posts-wip/rainbow-quox/pieces1.avif
new file mode 100644
index 0000000..dcad189
Binary files /dev/null and b/posts-wip/rainbow-quox/pieces1.avif differ
diff --git a/posts-wip/rainbow-quox/pieces2.avif b/posts-wip/rainbow-quox/pieces2.avif
new file mode 100644
index 0000000..4b3e60a
Binary files /dev/null and b/posts-wip/rainbow-quox/pieces2.avif differ
diff --git a/posts-wip/rainbow-quox/quoxes1.avif b/posts-wip/rainbow-quox/quoxes1.avif
new file mode 100644
index 0000000..3060729
Binary files /dev/null and b/posts-wip/rainbow-quox/quoxes1.avif differ
diff --git a/posts-wip/rainbow-quox/red.avif b/posts-wip/rainbow-quox/red.avif
new file mode 100644
index 0000000..1a45b94
Binary files /dev/null and b/posts-wip/rainbow-quox/red.avif differ
diff --git a/posts-wip/rainbow-quox/relative.avif b/posts-wip/rainbow-quox/relative.avif
new file mode 100644
index 0000000..93a16df
Binary files /dev/null and b/posts-wip/rainbow-quox/relative.avif differ
diff --git a/posts/chrismas.md b/posts/chrismas.md
index 08cfb13..d038f4d 100644
--- a/posts/chrismas.md
+++ b/posts/chrismas.md
@@ -1,7 +1,7 @@
---
date: 2023-12-25
title: merr chrismas
-tags: [lántas, conlangs]
+tags: [lántas, conlangs, fursona]
conlang: laantas
summary: |
how to say "merr chrismas" in my conlang lántas.
@@ -80,7 +80,11 @@ midwinter".
::: {.twocol-grid .light}
-{width=100%}
+
+
+
+
+
::: {.glosses .left}
- þugusim ai
@@ -90,7 +94,11 @@ midwinter".
- it crismas
:::
-{width=100%}
+
+
+
+
+
::: {.glosses .left}
- ufi þugusinhari
diff --git a/posts/chrismas/1.webp b/posts/chrismas/1.webp
new file mode 100644
index 0000000..463b3e6
Binary files /dev/null and b/posts/chrismas/1.webp differ
diff --git a/posts/chrismas/2.webp b/posts/chrismas/2.webp
new file mode 100644
index 0000000..fc57f89
Binary files /dev/null and b/posts/chrismas/2.webp differ
diff --git a/posts/cube.md b/posts/cube.md
index 4a54544..3a405a8 100644
--- a/posts/cube.md
+++ b/posts/cube.md
@@ -6,7 +6,7 @@ summary: >
i redesigned my personal website. it was a bit of an ordeal.
...
-{.floating .right}
+{.floating .right .expandable}
so for the past little while i've been making a big update to my [personal website]. it's a cube now! i wanted to make sure it worked in several browsers:
diff --git a/posts/cube/cube.webp b/posts/cube/cube.webp
new file mode 100644
index 0000000..1f4cafe
Binary files /dev/null and b/posts/cube/cube.webp differ
diff --git a/posts/first-person-pronouns.md b/posts/first-person-pronouns.md
new file mode 100644
index 0000000..2834419
--- /dev/null
+++ b/posts/first-person-pronouns.md
@@ -0,0 +1,129 @@
+---
+title: lántas pronoun update
+date: 2024-11-25
+tags: [lántas, conlangs]
+conlang: laantas
+summary: first-person neopronouns. and… neoinflections?
+...
+
+so my "main" conlang [`@lántas@`][l] is actually kind of old at this point. old enough that when i made the personal pronouns, i didn't know that plurality was a thing that existed, so until today, the first person pronouns were `{!ká}` in the singular, and `{!til}` in the [(grammatical)]{.note} plural. except that `{til}` is an [`@inclusive@`][clus] pronoun, meaning it can only be used when the listener is included. which, as you can see from the fact it has a wikipedia article, is a thing that real life languages do sometimes.
+
+[l]: https://lang.niss.website/laantas
+[clus]: https://en.wikipedia.org/wiki/Clusivity
+
+however, when someone uses "we" to mean "me and my headmates", that is (usually??) an exclusive usage. which means you can't use `{til}`, or the first-person plural verb inflection, and instead have to say `{#kakas rú, rúl}` `{kakas rú(l)}`, or "me and them". which is… pretty awkward.
+
+it's time to get a new one.
+
+# pronouns
+
+:::{.figure .hugescr .floating .right}
+`{#kál}`
+:::
+
+it seems that it would be pretty unlikely, given people's general _attitudes_, that a personal pronoun dedicated to plurality would arise naturally. so this is the perfect opportunity to have a `@neopronoun@`. without grammatical gender existing in the first place, there's no particular pressure for a new third-person pronoun to crop up. `{!rú}` (or `{!rúl}`) fits everyone just fine. as far as i know, anyway.
+
+so, `{!kál}`. it is pretty transparently the singular pronoun with the regular plural ending, `{!ká–l}`. but that's fine. it fits in with `{!rú}`, `{!rúl}` 'he/she/they (sg)/etc, they (pl)', and _almost_ with `{!sur}`, `{!sual}` 'you (sg)/you (pl)' too.
+
+`{!kál}` inflects almost like a regular noun with `{!ka–}` stem, except for the COM, which matches `{!tiksł}` and `{!ruksł}`, and the locative cases, which keep the long vowel like `{!ká}` does.
+
+in the table `!SPL!` stands for `@system plural@` i guess. (and `!IPL!` for `@inclusive plural@`; the old thing.)
+
+---
+header-includes: |
+
+...
+
+
+
+
+
1SG
+
1SPL
+
1EPL
+
+
NOM
+
`{!ká}`
+
`{!kál}`
+
`{!til}`
+
+
GEN
+
`{!kat}`
+
`{!katł}`
+
`{!tial}`
+
+
COM
+
`{!kakas}`
+
`{!kaksł}`
+
`{!tiksł}`
+
+
CAR
+
`{!kassa}`
+
`{!kassal}`
+
`{!tissal}`
+
+
INS
+
`{!kala}`
+
`{!kalal}`
+
`{!tilla}`
+
+
ESS
+
`{!kugu}`
+
`{!kugul}`
+
`{!tigul}`
+
+
TRA
+
`{!kasti}`
+
`{!kastil}`
+
`{!tistil}`
+
+
EXE
+
`{!kaču}`
+
`{!kačul}`
+
`{!tičul}`
+
+
LOC
+
`{!ká–}`
+
`{!ká–l}`
+
`{!tí–l}`
+
+
+
+see [§3–4 of the noun page][cases] for inadequate descriptions of these cases that one day i will maybe expand on.
+
+[cases]: https://lang.niss.website/laantas/nouns.html#corecases
+
+# verb inflections
+
+:::{.figure .hugescr .floating .right}
+`{#–káš}` `{#–kúš}`
+:::
+
+the existing [person suffixes][ps] for verbs actually have no resemblance at all to the pronouns. the new one does though. after all, it's new! it's `{!–káš}` for the subject and `{!–kúš}` for the object.
+
+[ps]: http://lang.niss.website/laantas/verbs.html#person
+
+
+
+
+
1SG
+
1SPL
+
1EPL
+
+
SBJ
+
`{!–na}`
+
`{!–káš}`
+
`{!–náš}`
+
+
OBJ
+
`{!–du}`
+
`{!–kúš}`
+
`{!–dúš}`
+
diff --git a/posts/goodbye-cohost.md b/posts/goodbye-cohost.md
new file mode 100644
index 0000000..955f34c
--- /dev/null
+++ b/posts/goodbye-cohost.md
@@ -0,0 +1,62 @@
+---
+title: goodbye cohost
+tags: [misc]
+date: 2024-10-01
+summary: thanks for being a website.
+header-includes: |
+
+...
+
+```{=html}
+
+
HIGH SCORE
+6969420 6969420
+
+ CONGRATURATIONS !!
+
+ NOW YOU SAVE EGGBUG
+ AND
+ THE ADVENTURE IS OVER
+
+ THANK YOU
+ FROM
+WEB SITE jkap
+ vogon
+GRAPHIC DESIGN aidan
+MODERATION kaara
+ AND
+ AMUSEMENT CREATER
+
+
+```
+
+thanks for being a website.
diff --git a/posts/goodbye-cohost/PressStart2P-Regular.ttf b/posts/goodbye-cohost/PressStart2P-Regular.ttf
new file mode 100644
index 0000000..1098ed2
Binary files /dev/null and b/posts/goodbye-cohost/PressStart2P-Regular.ttf differ
diff --git a/posts/goodbye-cohost/PressStart2P-Regular.woff2 b/posts/goodbye-cohost/PressStart2P-Regular.woff2
new file mode 100644
index 0000000..c6c87e4
Binary files /dev/null and b/posts/goodbye-cohost/PressStart2P-Regular.woff2 differ
diff --git a/posts/goodbye-cohost/cohost.svg b/posts/goodbye-cohost/cohost.svg
new file mode 100644
index 0000000..e43713e
--- /dev/null
+++ b/posts/goodbye-cohost/cohost.svg
@@ -0,0 +1 @@
+
diff --git a/posts/goodbye-cohost/hiscore.mp3 b/posts/goodbye-cohost/hiscore.mp3
new file mode 100644
index 0000000..041c78f
Binary files /dev/null and b/posts/goodbye-cohost/hiscore.mp3 differ
diff --git a/posts/qt-refsheet.md b/posts/qt-refsheet.md
new file mode 100644
index 0000000..1155d39
--- /dev/null
+++ b/posts/qt-refsheet.md
@@ -0,0 +1,92 @@
+---
+title: q.t. refsheet transcriptions
+date: 2024-11-26
+tags: [fursona, lántas, conlangs]
+conlang: laantas
+summary: quick post for the text on q.t.'s refsheet
+...
+
+:::figure
+
+
+
+:::
+
+fitting lántas into a strictly eight-pixel high font was… difficult. and involved a lot of special-casing. it would be a huge hassle to get a computer to do it automatically.
+
+anyway let's get to it
+
+:::{.glosses .left}
+- kuaksat pasaga
+- [ˈkɔə̯ksət ˌpasəɣɐ]
+- kuaksa-t pas-aga
+- quox-GEN two-body
+- quox taur
+
+---
+
+- #6# mitral. #19# fútkasł #8# inčil
+- [ˌdʒutːə ˈmitɾɐl ‖ ˌtaksɪːstʊ ˈfuːtkɑsɫ | ˌn̩daː ˈʔintʃiɬʲ]
+- ǧutta mitra-l. taks(a)-ístu fút-kas-ł ńdá inči-l
+- six metre-PL. ten-nine foot-COM-PL eight inch-PL
+- 6m. 19′ 8″
+
+---
+
+- #376666# kígíl
+- [ˌkɑɫːeˌbuʃɻ̩ ˌlivɪnɐˌtaksə ˌdʒutːəˌxɑːruəɬʲ dʒutːəbuʃɻ̩ ˌdʒutːɐtʃutːə ˈkɛːʝɛɬʲ]
+- kalli-bušŕ libina-taksa-ǧutta-hárual ǧutta-bušŕ ǧuttaččutta kígí-l
+- 3 76 6 66 kg-PL
+- 376,666 kg
+
+---
+
+- #829660# pundł
+- [ˌn̩daːˌbuʃɻ̩ ˌpastɐksˌiːstʊˌxɑːruəɬʲ ˌdʒutːəˌbuʃɻ̩ ˌdʒutːɐksə ˈpundɫ̩]
+- ńdá-bušŕ pas-taks(a)-ístu-hárual ǧutta-bušŕ ǧut(ta)-taksa pund(a)-ł
+- 8 29 6 60 pound-PL
+- 829,660 lb
+
+---
+
+- nakasnala samńt kaubal
+- [ˌnakɑsnɐlə ˈsamn̩t kɑʊvɐɬʲ]
+- na-kas-na-la samń-t kauba-l
+- one-COM-one-INS colour-GEN group-PL
+- all sets of colours
+:::
+
+:::aside
+btw, `{!nakasnai}`, literally "anything and anything", means "everything". i forgot which language i stole that from, sorry.
+
+it can be shortened to `{!násna}`, and its derived forms `{!nakasnala}` "every" and `{!nakasnanua}` "always" can be shortened to `{!násná}` [(ending with a long vowel)]{.note} and `{!násnua}` respectively.
+:::
+
+:::{.glosses .left}
+- násnua álitkiðkasł dilwitł ippau
+- [ˌnaːsnʊə ˈaːlɪtkɛθkɑsɫ̩ ˈdilwetɫ ipːɑʊ]
+- nakasna(i)-nua álit-kið-kas-ł dilwi-t-ł ippau
+- all-INTER neck-ring-COM sock-GEN-PL wear
+- always wears collars and socks
+
+---
+
+- ustaimł! panísat igisḿt ǧunaimkas pattal
+- [ˈustɐɪmɫ̩ ‖ pɐˌniːsɐt ˌiʝɛsm̩t ˈdʒnɐimkɑs ˈpatːaɬʲ]
+- ustai-m-ł panísa-t igis-ḿ-t ǧunai-m-kas patta-l
+- magic-DEF-PL blue-GEN crystal-DEF-GEN rod-DEF-COM portal-PL
+- magic! the blue crystal rod and portals
+
+---
+
+- kalli talaskasł nai usu liččali ai
+- [ˌkɑɫːe ˈtalɐskɑsɫ̩ ˌnæɪj‿ˈusʊ ˌlitːʃɐlɪj‿æɪ]
+- kalli talas-kas-ł nai usu ličča-li ai
+- three head-COM-PL one mind much-IN be
+- there are three heads but usually one mind
+
+:::
+
+you may notice some discrepancies between these squiggles and the squiggles on the refsheet. ~~oops! i'll fix em tomorrow.~~ it wasn't quite "tomorrow" but it's done now.
+
+well bye
diff --git a/posts/qt-refsheet/ref.webp b/posts/qt-refsheet/ref.webp
new file mode 100644
index 0000000..4561abe
Binary files /dev/null and b/posts/qt-refsheet/ref.webp differ
diff --git a/posts/quorientation.md b/posts/quorientation.md
index ed8084b..d40f526 100644
--- a/posts/quorientation.md
+++ b/posts/quorientation.md
@@ -1,16 +1,17 @@
---
date: 2024-03-14
title: quorientation
-tags: [lántas, conlangs]
+tags: [fursona, lántas, conlangs]
conlang: laantas
summary: |
in my latest art, i put some text in lántas. here is approximately
too much detail about that.
+header-includes:
...
-
+
@@ -40,7 +41,7 @@ you know! the thing! from the game!
well. from the fan translation
-
+
- out of context, `{!patta}` means door. i suppose a portal would be a magic
diff --git a/posts/quorientation/pic.webp b/posts/quorientation/pic.webp
new file mode 100644
index 0000000..780230b
Binary files /dev/null and b/posts/quorientation/pic.webp differ
diff --git a/posts/quorientation/skip-some-floors.png b/posts/quorientation/skip-some-floors.png
new file mode 100644
index 0000000..02e3623
Binary files /dev/null and b/posts/quorientation/skip-some-floors.png differ
diff --git a/sources/cube.kra b/sources/cube.kra
new file mode 100644
index 0000000..d95e7f3
Binary files /dev/null and b/sources/cube.kra differ
diff --git a/sources/rainbow-quox/blends.png b/sources/rainbow-quox/blends.png
new file mode 100644
index 0000000..8c9db40
Binary files /dev/null and b/sources/rainbow-quox/blends.png differ
diff --git a/sources/rainbow-quox/dark.png b/sources/rainbow-quox/dark.png
new file mode 100644
index 0000000..469bdba
Binary files /dev/null and b/sources/rainbow-quox/dark.png differ
diff --git a/sources/rainbow-quox/dark2.png b/sources/rainbow-quox/dark2.png
new file mode 100644
index 0000000..162f009
Binary files /dev/null and b/sources/rainbow-quox/dark2.png differ
diff --git a/sources/rainbow-quox/front.png b/sources/rainbow-quox/front.png
new file mode 100644
index 0000000..fdfc4a0
Binary files /dev/null and b/sources/rainbow-quox/front.png differ
diff --git a/sources/rainbow-quox/pieces1.kra b/sources/rainbow-quox/pieces1.kra
new file mode 100644
index 0000000..95372be
Binary files /dev/null and b/sources/rainbow-quox/pieces1.kra differ
diff --git a/sources/rainbow-quox/pieces2.kra b/sources/rainbow-quox/pieces2.kra
new file mode 100644
index 0000000..0aebab3
Binary files /dev/null and b/sources/rainbow-quox/pieces2.kra differ
diff --git a/sources/rainbow-quox/quoxes1.kra b/sources/rainbow-quox/quoxes1.kra
new file mode 100644
index 0000000..7388c3b
Binary files /dev/null and b/sources/rainbow-quox/quoxes1.kra differ
diff --git a/sources/rainbow-quox/quoxes1.png b/sources/rainbow-quox/quoxes1.png
new file mode 100644
index 0000000..8d42de0
Binary files /dev/null and b/sources/rainbow-quox/quoxes1.png differ
diff --git a/sources/rainbow-quox/red.png b/sources/rainbow-quox/red.png
new file mode 100644
index 0000000..925d5a4
Binary files /dev/null and b/sources/rainbow-quox/red.png differ
diff --git a/sources/rainbow-quox/relative.png b/sources/rainbow-quox/relative.png
new file mode 100644
index 0000000..395e0bd
Binary files /dev/null and b/sources/rainbow-quox/relative.png differ
diff --git a/style/page.css b/style/page.css
index 7394654..0eb0b8d 100644
--- a/style/page.css
+++ b/style/page.css
@@ -38,10 +38,9 @@
:root, body { margin: 0; padding: 0; }
-main {
- border-bottom: 2px dotted var(--fg);
+main, footer { max-width: 50rem; }
- max-width: 50em;
+main {
min-height: 100%;
margin: 1em auto 0;
padding: 0.5em 2em;
@@ -63,10 +62,13 @@ header {
header h1 {
font-size: 200%;
margin: 0;
+ font-weight: normal;
+ text-transform: uppercase;
+ letter-spacing: 0.4ch;
}
/* h1, h2, h3, h4, h5, h6 { */
-h1 {
+main h1 {
margin: 1em 0 0.25em;
font-weight: normal;
@@ -231,7 +233,7 @@ pre, :not(pre) > code {
pre, :not(pre) > code { background: hsla(0deg 0% 00% / 30%); }
}
-:not(pre) > code { padding: 0 5px; }
+:not(pre) > code { padding: 0 5px; white-space: nowrap; }
pre {
clear: both;
@@ -260,16 +262,20 @@ pre {
font-weight: normal;
}
-.gloss .abbr, .abbr-list dt {
+.abbr, .abbr-list dt {
font-variant: all-small-caps;
}
.scr {
height: 1.5em;
vertical-align: -40%;
- margin-right: 0.5ex;
- padding: 2px;
- background: var(--light);
+}
+
+@media (prefers-color-scheme: dark) {
+ .scr {
+ padding: 2px;
+ background: var(--light);
+ }
}
.gloss-split, .gloss-gloss {
@@ -280,6 +286,10 @@ pre {
height: 2em;
}
+.hugescr .scr {
+ height: 4em;
+}
+
:is(.splash, .example) .scr {
height: unset;
display: block;
@@ -344,15 +354,33 @@ blockquote {
figure img {
max-width: 100%;
}
-figure img:not(.scr) {
+figure:not(.nobg, .hasborder) img:not(.scr) {
border: 3px solid currentcolor;
}
+figure.nobg a img {
+ /* fake outline */
+ filter:
+ drop-shadow(1px 1px 0 currentcolor)
+ drop-shadow(1px -1px 0 currentcolor)
+ drop-shadow(-1px 1px 0 currentcolor)
+ drop-shadow(-1px -1px 0 currentcolor)
+ drop-shadow(1px 0 0 currentcolor)
+ drop-shadow(-1px 0 0 currentcolor)
+ drop-shadow(0 1px 0 currentcolor)
+ drop-shadow(0 -1px 0 currentcolor) ;
+}
+figure.lightbg img {
+ background: var(--light);
+}
figure:not(.left) {
text-align: center;
}
figure:not(.left) table {
display: inline-table;
}
+.twocol-grid figure {
+ margin: 0;
+}
figure table {
margin: 1em 0.5em;
}
@@ -376,6 +404,11 @@ figcaption {
line-height: 125%;
font-style: italic;
margin: 0 auto;
+ text-align: center;
+ text-wrap: balance;
+}
+figcaption em {
+ font-style: normal;
}
:not(.floating) > figcaption {
width: 75%;
@@ -428,6 +461,7 @@ u u {
footer {
clear: both;
+ border-top: 2px dotted var(--fg);
margin: 1.5em auto 3em;
font-size: 80%;
@@ -485,7 +519,7 @@ footer li + li::before { content: ' · '; }
}
blockquote {
- max-width: 70%;
+ max-width: 85%;
border-left: 1px solid black;
padding-left: 1em;
margin: auto;
@@ -500,6 +534,15 @@ blockquote {
font-style: italic;
}
+.banner {
+ font-size: 125%;
+ font-weight: bolder;
+ text-align: center;
+ text-wrap: balance;
+}
+.banner p:first-child::before { content: '☛ '; }
+.banner p:last-child::after { content: ' ☚'; }
+
:is(h1, h2) .note {
font-size: 75%;
}
@@ -596,6 +639,12 @@ aside.floating :last-child { margin-bottom: 0; }
vertical-align: -0.1em;
}
+.bigemoji {
+ height: 2em;
+ width: 2em;
+ vertical-align: -0.2em;
+}
+
.citation {
font-size: 90%;
- 
- 
+ 
+ 
+
+
+
+
+
+
+
+