Manuscript IX-Free@1 · IX-Free.tex · section · 33b20e96

Prerequisite ledger

Contract, inherited inputs, and domains › Prerequisite ledger · lines 432–444

The inherited preservation obligations, where a product has actually been defined, are

ι (A ⋆_{H} B) = ι (A) ⋆_{Σ} ι (B), C_{j}^{Σ} = C_{j}^{old} on specified common regular domains, cl (A ⋆_{Σ} B) = cl (A) cl (B) .

Here $cl$ denotes the order-zero projection. These are obligations, not conclusions about an unconstructed product.

Displayed formulas in this passage

unlabeled · line 436
$ι (A ⋆_{H} B) = ι (A) ⋆_{Σ} ι (B), C_{j}^{Σ} = C_{j}^{old} on specified common regular domains, cl (A ⋆_{Σ} B) = cl (A) cl (B) .$