self_types_with_sigma.md

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

While, traditionally, with self types you can do the inductive types, they require positive recursion and not only strictly positive recursion.

// bad 
Bool : Type;
true : Bool;
false : Bool;


Bool = (b : Bool) &
  // Bool in P is not strictly positive
  (P : (b : Bool) -> Type, t : P(true), f : P(false)) -> P(b);
// you may think about using polarity annotations
Bool = (b : Bool) &
  (P : (b : ++Bool) -> Type, t : P(true), f : P(false)) -> P(b);

// but this leads to a tweaked induction principle
// notice that P can only mention b in a strictly positive position
ind : (b : Bool) ->
  (P : (b : ++Bool) -> Type, t : P(true), f : P(false)) -> P(b);

// I'm not sure if it is possible to derive induction out of this

Almost Inductive Booleans

Let's go back to encoding booleans without self types for a second.

// notice this polarity annotation only on C_Bool;
// it will matter in the future

// church booleans
C_Bool : Type = (A : ++Type, t : A, f : A) -> A;
c_true : C_Bool = (A, t, f) => t;
c_false : C_Bool = (A, t, f) => f;

// induction principle for church booleans
I_Bool : (c_b : C_Bool) -> Type = (c_b) =>
  (P, t : P(c_true), f : P(c_false)) -> P(c_b);
i_true : I_Bool(c_true) = (P, t, f) => t;
i_false : I_Bool(c_false) = (P, t, f) => f;

// packaging them together
W_Bool : Type = [c_b : C_Bool, I_Bool(c_b)];
w_true : W_Bool = [c_true, i_true];
w_false : W_Bool = [c_false, i_false];

// can only do induction over fst(w_b)
w1_ind : (w_b : W_Bool) ->
  (P, t : P(c_true), f : P(c_false)) -> P(fst(w_b))
w1_ind = (w_b) => snd(w_b);

// but if fst(w_b)(_, w_true, w_false) == w_b
w2_ind : (w_b : W_Bool, h : fst(w_b)(_, w_true, w_false) == w_b) ->
  (P, t : P(w_true), f : P(w_false)) -> P(w_b)
w2_ind = (w_b, h) => (P, t, f) =>
  transport(
    P,
    h,
    w1_ind(w_b)
  );

Self Types Again

Instead of doing the self types to make the whole induction, we can use it to ensure that fst(w_b)(_, w_true, w_false) == w_b. This is related to splitting idempotents.

Bool : Type;
true : Bool;
false : Bool;

// the w_b
// 
Bool = (b : Bool) &
  // Bool here is only used in strictly positive positions
  [w_b : W_Bool, fst(w_b)(Bool, true, false) == b];
true = [w_true, refl()];
false = [w_false, refl()];

// then
ind : (b : Bool) -> (P, t : P(true), f : P(false)) -> P(b);
ind = (b) => (P, t, f) =>
  transport(
    P,
    // fst(fst(b))(_, true, false) == b
    snd(b),
    // P(fst(fst(b))(_, true, false))
    snd(fst(b))(c_b => P(c_b(_, true, false)), t, f)
  );