Cubical Type Theory (CTT)

cubical.agda

{--
Some informal notes on the talk Cubical Agda: A Dependently Typed Programming
Language with Univalence and Higher Inductive Types by Andrea Vezzosi.

Link: https://youtu.be/AZ8wMIar-_c
--}

--- Equality in dependently typed languages like Agda is defined as an inductive
--- family:
data _≡_ {A : Set} (x : A) : A →  Set where
    refl : x ≡ x

--- Any propery or type respects an equality; all closed elements reduce to
--- `refl`. Terms compute as expected in a closed context.
transport : (P : A →  Set) →  ∀ x y →  x ≡ y →  P x →  P y
transport P x x refl p = p

--- "List is the free monoid"
data List (A : Set) : Set where
    [] : List A
    _≡_ : A →  List A

--- as a higher inductive type, via axioms:
data FreeMonoid (A : Set) : Set where
    [_] : A →  FreeMonoid A
    _∊_ : FreeMonoid A
    _*_ : FreeMonoid A →  FreeMonoid A →  FreeMonoid A
    assoc : ∀ x y z →  x * (y * z) ≡ (x * y) * z

--- Free groups, via homotopy type theory:
data FreeGroup (A : Set) : Set where
    [_] : A →  FreeGroup A
    _∊_ : FreeGroup A
    _*_ : FreeGroup A →  FreeGroup A →  FreeGroup A
    _¹_ : FreeGroup A →  FreeGroup A
    assoc : ∀ x y z →  x * (y * z) ≡ (x * y) * z
    inv-left : ∀ x  →  x ¹ * x ≡ ∈

{--

A high level overview of univalence:
--------------
Types ⇒  Spaces
x ≡ A y ⇒  There is a path from x to y in A
i : I ⊢ t : A ⇒  path represented as a map [0,1] →  A
--------------
Univalence is thus a theorem and transports along it compute.
HITs have eliminators that compute on both point and path constructors.

Cubical Agda is an extension of Agda with support for cubical type theory.
https://github.com/agda/cubical

Features:
Nested pattern matching with HITs.
Bisimilarity as equality for coinductive types.
Interval as a type: I
Restriction types: A [ r ↣  u ]
--}