EduardoRFS

%{
open Utils
open Ctree

let mk (loc_start, loc_end) =
  Location.{ loc_start; loc_end; loc_ghost = false }

%}
%token <string> VAR (* x *)
%token COLON (* : *)

EduardoRFS

module Syntax = struct
  type var = string

  type term =
    | T_var of var
    | T_let of var * term * term
    | T_annot of term * term
    | T_with_self of term * term
    (* pi *)
    | T_forall of var * term * term

EduardoRFS

Pi-Sigma-Self

The following is a set of syntax-directed rules to typing a dependently type system with self types. This is hopefully decidable given decidable conversion checking.

The main innovation is that all introduction rules propagate the self due to the new type of checking rule. This allows the fixpoint to be transparent to introductions, when combined with pairs, this leads to mutual recursion and the inductive types.

This doesn't define any universe or restriction to fixpoints, as those are more or less orthogonal to the typing issues here.

Syntax

EduardoRFS

(* index when term, level when value *)
type var = int
type index = int
type level = int

type term =
  (* x *)
  | T_var of { var : var }
  (* x = M; N *)
  | T_let of { arg : term; body : term }

EduardoRFS

{
  "name": "Community-Material-Theme-Darker-High-Contrast",
  "type": "dark",
  "tokenColors": [
    {
      "settings": {
        "background": "#212121",
        "foreground": "#ffffff"
      }
    },

EduardoRFS

Set Universe Polymorphism.

Axiom Path : forall (A : Type), A -> A -> Type.
Axiom refl : forall {A x}, Path A x x.
Axiom transport : forall {A x y} (p : Path A x y),
  forall (P : A -> Type), P x -> P y.

Axiom transport_refl : forall {A x y} (p : Path A x y),
  transport p (fun z => Path A x z) refl = p.
Axiom transport_fst : forall {A x y} (p : Path A x y),

EduardoRFS

Induction-recursion in Impredicative Type Theory

When building universes in a type theory, the standard technique relies on induction-recursion, but Kovács points out that the logical consistency of induction-recursion and induction-induction in the context of impredicative type theory is an open question.

Lastly, we do not handle impredicative universes. The main reason for this is that we do not know the consistency of having induction-recursion and impredicative function space together in the same universe, and modeling impredicativity seems to require this assumption in the metatheory.

Here I will not be providing a mechanized proof, as that is still a work in progress, but two techniques to justify mutual definitions in type theories. The running example will be the following mutual definition, where N depends on the value of x.

x : A;

EduardoRFS

Inductive D : bool -> Type :=
  | c0 : D true
  | c1 : D false.

Lemma prove_me_general b : forall (v : D b),
  v =  match b with | true => c0 | false => c1 end.
Proof.
  intros v.
  induction v; reflexivity.
Qed.

EduardoRFS

(*
  Everything here is really ugly as I didn't clean it,
    some bits come from the Coq-HoTT library.

  The main idea is that given funext and any
    h-set with multiple provably distinct elements.

  Univalence is only used to prove s_true_neq_s_false

  Then by funext you can get the induction principle to contract.

EduardoRFS

Require Import List.
Import ListNotations.
Require Import Bool.
Require Import PeanoNat.
Require Import Lia.

Definition Index := nat.
Definition Level := nat.

Inductive Term :=