qexat

induct _=_ {T} _ _ ≔
  rule reflexivity x. (x : T) -> (Refl x : x = x)
with module
  rule symmetry x y. x = y -> y = x ≔ λ (Refl x) → Refl x
  rule transitivity x y z. x = y -> y = z -> x = z ≔
    fun x-=-y y-=-z → (x-=-y)[ϕ y-=-z]
end

induct _×_ A B ≔
  rule pair x y. (x : A) -> (y : B) -> ('(x, y') : A × B) 

qexat

Require Import Arith.

Lemma max_override_right : forall (n m p : nat), (n >= m) -> max n (max m p) = max n p.
Proof.
  intros n m p ge_n_m.

  inversion ge_n_m ; rewrite Nat.max_assoc.
  - rewrite Nat.max_id.
    reflexivity.
  - rewrite H0.

qexat

data Nat where
  O :: Nat
  S :: Nat -> Nat

instance Eq Nat where
  (==) O O = True
  (==) O (S _) = False
  (==) (S _) O = False
  (==) (S n) (S m) = n == m

qexat

let ( let+ ) = Option.bind

module Expr = struct
  type app = A
  type fun' = F
  type name = N
  type 'variant reducible = A : app reducible

  type 'variant irreducible =
    | F : fun' irreducible

qexat

module type TYPE = sig
  type t
end

type 't module' = (module TYPE with type t = 't)
type 'a first = 'b constraint 'a = 'b * _
type 'a second = 'c constraint 'a = _ * 'c

module Runtype = struct
  type 'a t =

qexat

let get_char () =
  let attr = Unix.tcgetattr Unix.stdin in
  let () =
    Unix.tcsetattr
      Unix.stdin
      Unix.TCSADRAIN
      { attr with Unix.c_icanon = false }
  in
  let res = input_byte stdin in
  Unix.tcsetattr Unix.stdin Unix.TCSADRAIN attr;

qexat

module Option = struct
  include Option

  let or_else : type item. (unit -> item t) -> item t -> item t =
    fun rightf left ->
    match left with
    | None -> rightf ()
    | _ -> left
  ;;

qexat

tokens:
  INFINITY ≔ '∞'
  ZERO ≔ '0'
  ONE ≔ '1'
  NONZERO ≔ /[1-9][0-9]*/
  QUESTION_MARK ≔ '?'
  BANG ≔ '!'

  NAME ≔ /[A-Za-z_][A-Za-z0-9_']*/
  CONTAINS ≔ '∋'

qexat

Require Import Utf8.

(** [Eqw f x y] represents the equivalence x y up to an isomorphism f. *)
Inductive Eqw {A B : Type} (f : A → B) : A → A → Prop :=
  | Refl (x y : A) : f x = f y → Eqw f x y.

(** Notation for convenience. Same level as equality. *)
Notation "x = y 'up' 'to' f" := (Eqw f x y).

(** Utilitary functions for the theorems below. *)

qexat

Require Import String.

Inductive Term : nat -> Type :=
  | App : forall {n m : nat}, Term (S n) -> Term m -> Term (n + m)
  | Fun : forall {n : nat}, Term 0 -> Term n -> Term (S n)
  | Var : string -> Term 0.