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 :=

EduardoRFS

Self Types + Sigma for Induction

This is a different technique that can be used for self types in more traditional MLTT settings, by doing induction through pairs instead of functions.

This idea was inspired by a comment from Ryan Brewer on the PLD Discord server. Paraphrasing it something, something inductive types positives so pairs.

edit: As pointed out by Ryan Brewer, I hallucinated half of the message ...

Self Typed Booleans

EduardoRFS

Positive vs Negative encoded streams

This shows some relations between positively and negatively encoded streams using self types, at the end we conclude that one is definitionally equal to the other if sigma is also encoded as an inductive type with self types.

I would claim that given the relation here, any advantage of one over the other is a matter of ergonomics and the implementation quality.

A nice bit to think later is about extensionalities of those?

So, what did Coq and Agda got wrong?

EduardoRFS

type var = int

type term =
  (* x *)
  | T_var of var
  (* M N *)
  | T_apply of term * term
  (* x => M *)
  | T_lambda of var * term

EduardoRFS

N4 =
  | O
  | S
  | mod4 : Z == S(S(S(S(Z))));

B_N4 = (l : Bool, r : Bool);

in : _;

EduardoRFS

Definition Eq {A} (x y : A) := forall (P : A -> Type), P x -> P y.
Definition refl {A} {x : A} : Eq x x := fun P p_x => p_x.
Definition symm {A} {x y : A} (H : Eq x y) : Eq y x :=
  fun P p_y => H (fun z => P z -> P x) (fun x => x) p_y.

Lemma L_must_be_true (
  L_is_false : forall {T} {x y : T} (H : Eq x y),
    Eq H (fun P => symm H (fun z => P z -> P y) (fun x => x)) -> False
  ) : False.
  exact (L_is_false _ I I refl refl).

EduardoRFS

type term =
  | APP of term * term
  | VAR of var
  | FST of dup
  | SND of dup
  | SUP of term * term
  | LAM of var * term
  | NIL

and var = { mutable var : term }