Syntax for pattern matching QIT (and maybe HIT) in OTT (and maybe HOTT) [blog/qit-syntax]

  • 2026/8/10

By OTT, we mean Loïc Pujet and Nicolas Tabareau’s Impredicative Observational Equality.

A type   a : A   b : A 
------------------------
    a ~_A b : Prop

cast A B : A ~_U B → A → B

Open Data Types

In OCaml (and a proposal of Haskell), there is a feature alowing you to extend a data type with new constructors. Which is called “Extensible Variant Types” in OCaml, and “Open Data Types” in Haskell. For some reasons, it is never supported by GHC.

In OCaml, the eliminator (pattern matching) of an extensible type should always have a default case for the future extended constructors. While in Haskell, the eliminator of an open data type is an open function, a function defined with pattern matching that can adding new clauses. For example

open data Expr = Add Expr Expr 

open pp : Expr → String 
pp (Add a b) = pp a ++ " + " ++ pp b 

data Expr += Lit Int 
pp (Lit x) = show x

Those features can work perfectly with Agda style pattern matching syntax.

A Syntax for QIT in Non Cubical TT

In CuTT (and XTT), A HIT should be considered as an inductive type with “boundary conditions”, and functions should eliminate such types with respect to the conditions. But in OTT, we do not have such thing.

Basically, this note works out a syntax for, 1. how to define a QIT 2. how to eliminate it.

Define a QIT

Suppose there are indexed inductive types Eq_A a b : Prop over all QIT A where a b : A. (Note. For cubical indexed inductive types, we need to add a new constructor transpX. In OTT, we need the similar thing, but Eq is a irrelevent proposition family, we can omit that on it, because we do not need to compute a proposition)

The observational equality ~ computes to Eq when acting on QIT. i.e.

a ~_A b = Eq_A a b    for QIT A.

Thus we can translate a QIT, for example, the interval as follow,

data I : Type where 
  i0 i1 : I 

data EqI : I → I → Prop where 
  seg : i0 ~ i1

For indexed inductive types,

data Ty : Cx → Type where 
  ... 
  _[_] : {G D : Cx} → Ty D → Sb G D → Ty G 

data EqTy {G : Cx} : Ty G → Ty G → Prop where 
  ...
  id[] : A [ id ] ~ A

-- A ~_{Ty G} B = EqTy {G} A B

The sur-syntax is as usual,

data I : Type where 
  i0 i1 : I 
  seg : i0 ~ i1 

data Ty : Type where 
  ... 
  _[_] : {G D : Cx} → Ty D → Sb G D → Ty Γ
  ... 
  id[] : A [ id ] ~ A

Eliminate a QIT

We define an open indexed inductive type,

A : U i   x : A ⊢ B : U j 
----------------------------- Formation
 '(x : A) → B : U (imax i j)

f : '(x : A) → B    a : A
--------------------------- Elimination
f $ a : B [ a / x ]

Sometimes we omit $, just write f a.

The introduction and computation rules are generated by pattern matching functions. For example, when we have the following definition,

add : ℕ → ℕ → ℕ 
add zero    y = y
add (suc x) y = suc (x + y)

We actually defined,

add : 'ℕ → ℕ → ℕ -- an introduction rule, so add is a constructor
(add $ zero) = λ y → y -- a computation rule
(add $ (suc x)) = λ y → suc (add x y) -- a computation rule

The elaborator should insert ' and $ automatically.

Note. ($) is an open function.

We have another open function for '(x : A) → B

apd : (f : '(x : A) → B) (e : u ~_A v) → cast B[u] B[v] (ap B[_] e) (f u) ~ f v

apd is a trivial function and can be automatically generated, if A is just a non-quotient inductive type. So we focus only on the case when A is a QIT.

Every time we pattern match a QIT, e.g.

f : 'I → Bool 
f $ i0 = true
f $ i1 = true

Then apd is lacking a clause for f.

apd f (e : a ~_I b) = ...

we can split on e, because a ~_I b is a inductive type (Eq_I).

apd f (seg : i0 ~_I i1) = ... : f i0 ~_Bool f i1

f i0 = true = f i1, so the hole can be filled by refl

apd f seg = refl

I hope all of these can make sense in some way, and I will try to write a experimental implementation of it to see if it works. XD

Examples

===============

  F : I -> Bool -> Bool
  F i0 true = true 
  F i0 false = false
  F i1 true = true 
  F i1 false = false

  find elimination F : 'I -> Bool -> Bool
  missing apd clause
    apd {a} {b} F (e : a ~_I b) : F a ~ F b

===============

  f : I -> I -> Bool
  f i0 i0 = True
  f i0 i1 = False
  f i1 i0 = True
  f i1 i1 = False

  find elimination f : 'I -> I -> Bool
  missing apd clause
    apd {a} {b} f (e : a ~_I b) : f a ~ f b 

  find elimination f (x : I) : 'I -> Bool
  missing apd clause 
    apd {a} {b} (f x) (e : a ~_I b) : f x a ~ f x b

  x can be further eliminated in apd
    apd {a} {b} (f i0) e = ...
    apd {a} {b} (f i1) e = ...

  no need to proof congruence for apd

in apd POV, f and F are constructors in pattern matching sense we don’t need to prove congruence if the target of elimination is a prop

Intuition:

  • '(x : A) -> B is an open indexed inductive type, indexed by A and x.B,each functor defined with pattern matching on A is a constructor to this type.
  • a ~_A b is an indexed inductive type over A,each quotient path is a new constructor to this type.
  • apd is an open function eliminating '(x : A) -> B and a ~_A b, for quotient inductive type A.when '(x : A) -> B is extended, the apd function should also be extended with new clauses,which corresponds to the congruence.