STLC Sums and Products

This extension adds ordinary product and coproduct forms. The surface layer still only translates syntax: products elaborate to Sigma, sums elaborate to the generated sum datatype, and case analysis elaborates to sumElim.

Products

A product type is a non-dependent Sigma. Pair introduction and projections reuse the existing HOAS pair, fst, and snd terms.

sigma = name: fst: snd: surface.mk "sigma" { inherit name fst snd; };
prod = fst: snd: sigma "_" fst (_: snd);
pair = fst: snd: surface.mk "pair" { inherit fst snd; };
fst_ = pair: surface.mk "fst" { inherit pair; };
snd_ = pair: surface.mk "snd" { inherit pair; };

natBoolProduct = prod H.nat H.bool;
natBoolPair = pair H.zero H.true_;
natBoolPairAnn = Core.ann natBoolPair natBoolProduct;

Sums

Sum injections keep both sides of the type explicit so the generated datatype constructors are inferable. Case analysis uses a constant motive for the STLC fragment.

sum = left: right: surface.mk "sum" { inherit left right; };
inl = left: right: term: surface.mk "inl" { inherit left right term; };
inr = left: right: term: surface.mk "inr" { inherit left right term; };
case_ = left: right: result: scrut: onLeft: onRight:
  surface.mk "case" { inherit left right result scrut onLeft onRight; };

stlcSumCaseChecks =
  let
    term = case_ H.nat H.bool H.nat leftZeroAnn
      (n: n)
      (_: H.zero);
    r = check term H.nat { path = [ "sum" "case" ]; };
  in
  !(r ? error);