transport_b4.md

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

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

in : _;
in = n4 =>
  match n4 with
  | Z => (false, false)
  | S(Z) => (false, true)
  | S(S(Z)) => (true, false)
  | S(S(S(Z))) => (true, true)
  | S(S(S(S(n4)))) => in(n4);
  end;
out = bn4 =>
  match bn4 with
  | (false, false) => Z
  | (false, true) => S(Z)
  | (true, false) => S(S(Z))
  | (true, true) => S(S(S(Z)))
  end;

H : N4 == B_N4 = ua(in, out, _);

incr = n4 => S(n4);
b_incr = transport<T => (x : T) -> T>(H, incr);
// eliminate transport
b_incr = b4 =>
  n4 = out(b4);
  r = incr(n4);
  in(r);
// inline incr and out
b_incr = b4 =>
  r =
    match b4 with
    | (false, false) => S(Z)
    | (false, true) => S(S(Z))
    | (true, false) => S(S(S(Z)))
    | (true, true) => S(S(S(S(Z))))
    end;
  in(r);
// move in to inside of the match
b_incr = b4 =>
  match b4 with
  | (false, false) => in(S(Z))
  | (false, true) => in(S(S(Z)))
  | (true, false) => in(S(S(S(Z))))
  | (true, true) => in(S(S(S(S(Z)))))
  end;
// betas in
b_incr = b4 =>
  match b4 with
  | (false, false) => (false, true)
  | (false, true) => (true, false)
  | (true, false) => (true, true)
  | (true, true) => (false, false)
  end;