Rezk Types

Rezk Types Skill

"In a Rezk type, isomorphisms are equivalent to identities — local univalence." — Emily Riehl & Michael Shulman

Overview

Rezk types are Segal types with an additional local univalence condition: categorical isomorphisms are equivalent to type-theoretic identities. This is the ∞-categorical analogue of the univalence axiom.

Core Definitions (Rzk)

#lang rzk-1

-- Isomorphism in a Segal type
#define is-iso (A : Segal) (x y : A) (f : hom A x y) : U
  := Σ (g : hom A y x), 
     (hom2 A x y x f g (id x)) × (hom2 A y x y g f (id y))

-- The type of isomorphisms
#define Iso (A : Segal) (x y : A) : U
  := Σ (f : hom A x y), is-iso A x y f

-- Identity-to-isomorphism map
#define id-to-iso (A : Segal) (x y : A) : (x = y) → Iso A x y
  := λ p. transport (λ z. Iso A x z) p (id x, refl-iso)

-- Rezk condition (local univalence)
#define is-rezk (A : Segal) : U
  := (x y : A) → is-equiv (id-to-iso A x y)

-- Rezk type (complete Segal space)
#define Rezk : U
  := Σ (A : Segal), is-rezk A

Chemputer Semantics

GF(3) Triad

segal-types (-1) ⊗ directed-interval (0) ⊗ rezk-types (+1) = 0 ✓

As a Generator (+1), rezk-types creates:

• Complete categorical structure
• Univalent foundations for chemistry
• Equilibrium-respecting species identification

The Local Univalence Principle

In a Rezk type:

(A ≅ B) ≃ (A = B)

Chemical interpretation: Two species at mutual equilibrium can be identified. The equilibrium constant K = 1 means "same species up to naming."

Lean4 Integration

import InfinityCosmos.ForMathlib.AlgebraicTopology.Quasicategory

-- Rezk completion functor
def RezkCompletion : SegalSpace → RezkSpace := sorry

-- Local univalence
theorem local_univalence (R : RezkSpace) (x y : R.X 0) :
    (x = y) ≃ Iso R x y := by
  exact R.rezk x y

Integration with Interaction Entropy

# Rezk completion for interaction sequences
module RezkCompletion
  # Two interaction sequences are "Rezk-equivalent" if
  # they produce the same observable effect
  
  def self.equivalent?(seq1, seq2)
    # Check if there's an isomorphism between outcomes
    # Isomorphism = both directions have GF(3) = 0
    forward_trit_sum = seq1.zip(seq2).map { |a, b| a.trit - b.trit }.sum
    backward_trit_sum = seq2.zip(seq1).map { |a, b| a.trit - b.trit }.sum
    
    (forward_trit_sum % 3 == 0) && (backward_trit_sum % 3 == 0)
  end
end

Key Theorems

1. Rezk completion exists: Every Segal type has a universal Rezk completion.

2. Functors preserve Rezk: A functor F : A → B between Rezk types preserves isomorphisms.

3. Adjoint is property: For a functor between Rezk types, having an adjoint is a mere proposition (at most one adjoint up to iso).

References

• Rezk, C. (2001). "A model for the homotopy theory of homotopy theory." Trans. AMS.
• Riehl, E. & Shulman, M. (2017). "A type theory for synthetic ∞-categories."
• sHoTT library