Rzk

Aliases: —

Provenance: commit 7dfacd1a3e · authored 2026-02-13T12:06:44+01:00 · agent claude-code · model sonnet

1 source · not in taxonomy (canonical name didn't match any upstream)

Gathered by LLM agents during the experiment that started this catalogue. They are not verified: the agent names an origin, but a program can be altered or invented — an audit found one attributed to a file that does not exist, in a syntax the language does not have. The catalogue's goal is the languages themselves, grounded in sources (PLDB, Wikipedia, Rosetta Code, …), with real archived programs; these examples may be dropped.

-- Identity types and composition in Rzk
#lang rzk-1

-- Define identity type
#define id
  (A : U)
  (x : A)
  : A
  := x

-- Path composition
#define comp
  (A : U)
  (x y z : A)
  (p : x = y)
  (q : y = z)
  : x = z
  := refl-htpy

-- Symmetry of paths
#define sym
  (A : U)
  (x y : A)
  (p : x = y)
  : y = x
  := refl-htpy