Визуализация диаграмм

Начиная с версии 0.3.0, rzk поддерживает визуализацию топов, типов и термов в виде диаграмм.

Это литературный файл rzk:

#lang rzk-1

Чтобы включить визуализацию диаграм, установите опцию "render" в "svg" или "latex" (чтобы отключить, используйте "none"):

#set-option "render" = "svg"  -- включить рендеринг диаграм в SVG
#set-option "render" = "latex"  -- включить рендеринг диаграм в LaTeX
#set-option "render" = "none"  -- отключить рендеринг диаграм

Для остальной части этой страницы используется SVG-рендеринг:

#set-option "render" = "svg"

Визуализация полностью автоматическая и работает в следующих ситуациях:

1. Отображение из формы (включая каррированные отображения), до 3 измерений, только в произведениях направленных интервалов 2;
2. Тип отображения из формы (включая каррированные отображения), до 3 измерений, только в произведениях направленных интервалов 2.
3. Отображения из формы, которая является сечением существующей формы.

Визуализация присваивает следующие цвета:

• фиолетовый присваивается переменным параметров (контекста);
• синий используется для заполнений типов (например, для hom и hom2);
• красный используется для термов (например, Segal-comp-witness);
• оранжевый используется для фигур в слое топов;
• серый используется для отброшенных частей (большего) отображения (например, при извлечении диагонали/грани из большей формы).

SVG изображения могут быть вставлены непосредственно в файлы .md перед соответствующим блоком кода rzk. Внизу .md файла вы можете добавить стилизацию, используя HTML-тег <style> и стили CSS, например:

<style>
  .rzk-render {
    transition: transform 0.2s; /* Анимация */
  }
  .rzk-render:hover {
    transform: scale(
      1.5
    ); /* (150% увеличение - Примечание: если увеличение слишком большое, оно выйдет за пределы области просмотра) */
  }
</style>

<!-- Определения для SVG изображений выше -->
<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>

Примеры

Визуализация симплициальных топов

Топы визуализируются оранжевым цветом:

-- 2-симплекс
#define Δ²
  : ( 2 × 2) → TOPE
  := \ (t , s) → s ≤ t

Граница топа:

-- граница 2-симплекса
#define ∂Δ²
  : Δ² → TOPE
  := \ (t , s) → s ≡ 0₂ ∨ t ≡ 1₂ ∨ s ≡ t

Самая сложная диаграмма топа включает весь 3D куб:

-- 3-мерный куб
#define 2³
  : ( 2 × 2 × 2) → TOPE
  := \ _ → TOP

-- 3-симплекс
#define Δ³
  : ( 2 × 2 × 2) → TOPE
  := \ ((t1 , t2) , t3) → t3 ≤ t2 ∧ t2 ≤ t1

Визуализация симплициальных типов

Типы визуализируются синим цветом. Распознанная параметрическая часть (например, фиксированные конечные точки, рёбра, грани с явными метками) визуализируется фиолетовым цветом. Когда тип строится путём взятия части другой формы, остальная часть большей формы окрашивается серым цветом.

-- [RS17, Определение 5.1]
-- Тип стрелок в A от x до y.
#define hom
  ( A : U)   -- Тип A.
  ( x y : A) -- Две точки в A.
  : U                   -- (hom A x y) это 1-симплекс (стрелка)
  := (t : 2) → A [ -- в A, где
    t ≡ 0₂ ↦ x , -- * левая конечная точка точно x
    t ≡ 1₂ ↦ y     -- * правая конечная точка точно y
  ]

-- [RS17, Определение 5.2]
-- тип коммутативных треугольников в A
#define hom2
  ( A : U)           -- Тип A.
  ( x y z : A)       -- Три точки в A.
  ( f : hom A x y)   -- Стрелка в A от x до y.
  ( g : hom A y z)   -- Стрелка в A от y до z.
  ( h : hom A x z)   -- Стрелка в A от x до z.
  : U                           -- (hom2 A x y z f g h) это 2-симплекс (треугольник)
  := ((t1 , t2) : Δ²) → A [   -- в A, где
    t2 ≡ 0₂ ↦ f t1 , -- * верхнее ребро точно f,
    t1 ≡ 1₂ ↦ g t2 , -- * правое ребро точно g, и
    t2 ≡ t1  ↦ h t2  -- * диагональ точно h
  ]

Визуализация термов симплициальных типов

Термы (с нетривиальными метками) визуализируются красным цветом (вы можете увидеть детальную метку при наведении). Распознанная параметрическая часть (например, фиксированные конечные точки, рёбра, грани с явными метками) визуализируется фиолетовым цветом. Когда терм строится путём взятия части другой формы, остальная часть большей формы окрашивается серым цветом.

Мы можем визуализировать термы, которые заполняют форму:

#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))

Если терм извлекается как часть большей формы, как правило, будет показана вся форма (серым цветом):

#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)