Function quot_env

crates/kernel/src/tutorial/reduction.rs:1467–1628

Build Quot environment: Quot, Quot.mk, Quot.lift, Quot.ind as KConst::Quot. Also includes Eq as full inductive (needed for Quot.lift validation).

()

        name: mk_name("Quot"),
        level_params: vec![mk_name("u")],
        kind: QuotKind::Type,
        lvls: 1,
        ty: quot_ty,
      },
    );

    // Quot.mk.{u} : {α : Sort u} → (r : α → α → Prop) → α → Quot r
    // depth 2 (inside α, r): α=var(1), r=var(0)
    // depth 3 (inside a): a=var(0), r=var(1), α=var(2)
    //   Quot α r = app(app(Quot.{u}, var(2)), var(1))
    let quot_mk_ty = ipi(
      "α",
      sort(param(0)),
      npi(
        "r",
        pi(var(0), pi(var(1), sort0())),
        npi("a", var(1), app(app(cnst("Quot", &[param(0)]), var(2)), var(1))),
      ),
    );
    env.insert(
      mk_id("Quot.mk"),
      KConst::Quot {
        name: mk_name("Quot.mk"),
        level_params: vec![mk_name("u")],
        kind: QuotKind::Ctor,
        lvls: 1,
        ty: quot_mk_ty,
      },
    );

    // Quot.lift.{u,v} :
    //   {α : Sort u} → {r : α → α → Prop} → {β : Sort v} →
    //   (f : α → β) → (h : ∀ a b, r a b → f a = f b) → Quot r → β
    //
    // d0: α
    // d1: r. α=var(0)
    // d2: β. r=var(0), α=var(1)
    // d3: f. β=var(0), r=var(1), α=var(2). f : α → β = pi(var(2), var(1))
    //   Inside f's pi: var(0)=arg, var(1)=β, var(2)=r, var(3)=α. body=var(1)=β ✓
    // d4: h. f=var(0), β=var(1), r=var(2), α=var(3)
    //   h : ∀ (a b : α), r a b → Eq.{v} β (f a) (f b)
    //   d5: a. a=var(0), f=var(1), β=var(2), r=var(3), α=var(4)
    //   d6: b. b=var(0), a=var(1), f=var(2), β=var(3), r=var(4), α=var(5)
    //     r a b = app(app(var(4), var(1)), var(0))
    //     d7: (inside r a b →)
    //       f a = app(var(3), var(2)), f b = app(var(3), var(1))
    //       Eq.{v} β (f a) (f b) = eq_expr(param(1), var(4), app(var(3), var(2)), app(var(3), var(1)))
    //   h_ty = npi("a", var(3), npi("b", var(4),
    //     pi(app(app(var(4), var(1)), var(0)),
    //       eq_expr(param(1), var(4), app(var(3), var(2)), app(var(3), var(1))))))
    // d5: (inside h). h=var(0), f=var(1), β=var(2), r=var(3), α=var(4)
    //   Quot r → β: pi(Quot α r, β)
    //   Quot α r = app(app(Quot.{u}, var(4)), var(3))
    //   d6: (inside pi) β = var(3)
    let f_ty = pi(var(2), var(1)); // α → β at d3
    let h_ty = npi(
      "a",
      var(3),