Rendering Diagrams

Starting from version 0.3.0, rzk supports rendering of topes, types, and terms as diagrams.

This is a literate rzk file:

#lang rzk-1

To enable rendering, set the option "render" to "svg" or "latex" (to disable, use "none"):

#set-option "render" = "svg"  -- enable rendering in SVG
#set-option "render" = "latex"  -- enable rendering in LaTeX
#set-option "render" = "none"  -- disable rendering

Rendering is completely automatic, and works in the following situations:

1. Mapping from a shape (including curried mappings), up to 3 dimensions, only in products of 2 cubes;
2. Type of mapping from a shape (including curried mappings), up to 3 dimensions, only in products of 2 cubes.
3. Mappings from a shape that is a section of an existing shape.

The rendering assigns the following colors:

• purple is assigned for parameters (context) variables;
• blue is used for fillings for types (e.g. for hom and hom2);
• red is used for terms (e.g. Segal-comp-witness);
• orange is used for shapes in the tope layer;
• grey is used for discarded parts of a (larger) mapping (e.g. when extracting a diagonal/face from a larger shape).

The SVG pictures can be inserted directly into .md files before a corresponding rzk code block. At the bottom of a markdown file, you might want to add stylization, e.g.:

<style>
  .rzk-render {
    transition: transform 0.2s; /* Animation */
  }
  .rzk-render:hover {
    transform: scale(
      1.5
    ); /* (150% zoom - Note: if the zoom is too large, it will go outside of the viewport) */
  }
</style>

<!-- Definitions for the SVG images above -->
<svg width="0" height="0">
  <defs>
    <style data-bx-fonts="Noto Serif">
      @import url(https://fonts.googleapis.com/css2?family=Noto+Serif&display=swap);
    </style>
    <marker
      id="arrow"
      viewBox="0 0 10 10"
      refX="5"
      refY="5"
      markerWidth="5"
      markerHeight="5"
      orient="auto-start-reverse"
    >
      <path d="M 0 2 L 5 5 L 0 8 z" stroke="purple" fill="purple" />
    </marker>
  </defs>
  <style>
    text,
    textPath {
      font-family: Noto Serif;
      font-size: 28px;
      dominant-baseline: middle;
      text-anchor: middle;
    }
  </style>
</svg>

Examples

Visualising Simplicial Topes

Topes are visualised with orange color:

-- 2-simplex
#define Δ²
  : ( 2 × 2) → TOPE
  := \ (t , s) → s ≤ t

Boundary of a tope:

-- boundary of a 2-simplex
#define ∂Δ²
  : Δ² → TOPE
  := \ (t , s) → s ≡ 0₂ ∨ t ≡ 1₂ ∨ s ≡ t

The busiest tope diagram involves the entire 3D cube:

-- 3-dim cube
#define 2³
  : ( 2 × 2 × 2) → TOPE
  := \ _ → TOP

-- 3-simplex
#define Δ³
  : ( 2 × 2 × 2) → TOPE
  := \ ((t1 , t2) , t3) → t3 ≤ t2 ∧ t2 ≤ t1

Visualising Simplicial Types

Types are visualised with blue color. Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with purple color. When a type is constructed by taking a part of another shape, the rest of the larger shape is colored using gray color.

-- [RS17, Definition 5.1]
-- The type of arrows in A from x to y.
#define hom
  ( A : U)   -- A type.
  ( x y : A) -- Two points in A.
  : U                   -- (hom A x y) is a 1-simplex (an arrow)
  := (t : 2) → A [ -- in A where
    t ≡ 0₂ ↦ x , -- * the left endpoint is exactly x
    t ≡ 1₂ ↦ y     -- * the right endpoint is exactly y
  ]

-- [RS17, Definition 5.2]
-- the type of commutative triangles in A
#define hom2
  ( A : U)           -- A type.
  ( x y z : A)       -- Three points in A.
  ( f : hom A x y)   -- An arrow in A from x to y.
  ( g : hom A y z)   -- An arrow in A from y to z.
  ( h : hom A x z)   -- An arrow in A from x to z.
  : U                           -- (hom2 A x y z f g h) is a 2-simplex (triangle)
  := ((t1 , t2) : Δ²) → A [   -- in A where
    t2 ≡ 0₂ ↦ f t1 , -- * the top edge is exactly f,
    t1 ≡ 1₂ ↦ g t2 , -- * the right edge is exactly g, and
    t2 ≡ t1  ↦ h t2  -- * the diagonal is exactly h
  ]

Visualising Terms of Simplicial Types

Terms (with non-trivial labels) are visualised with red color (you can see a detailed label on hover). Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with purple color. When a term is constructed by taking a part of another shape, the rest of the larger shape is colored using gray color.

We can visualise terms that fill a shape:

#define square
  ( A : U)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  ( h : hom A x z)
  ( a : Σ (h' : hom A x z) , hom2 A x y z f g h')
  : ( 2 × 2) → A
  := \ (t , s) → recOR(s ≤ t ↦ second a (t , s) , t ≤ s ↦ second a (s , t))

If a term is extracted as a part of a larger shape, generally, the whole shape will be shown (in gray):

#define face
  ( A : U)
  ( x y z : A)
  ( f : hom A x y)
  ( a : Σ (g : hom A y z)
        , ( ( ( t1 , t2) , t3) : 2 × 2 × 2 | t3 ≤ t1 ∨ t2 ≤ t1)
          → A [ t1 ≡ 0₂ ↦ f t2
              , t1 ≡ 1₂ ↦ g t3 ])
  : Δ² → A
  := \ (t , s) → second a ((t , t) , s)