carrierEquiv
plain-language theorem explainer
The definition supplies a canonical equivalence between any sort α and its CarrierType wrapper. Researchers handling universe-polymorphic carriers in RecogSpec cite it to align Sort u data with Type u APIs. The construction is a direct equivalence whose inverses hold by reflexivity.
Claim. For any sort α of universe level u there is an equivalence α ≃ CarrierType(α), where CarrierType(α) is the wrapper CarrierWrap(α).
background
The module supplies universe helpers and shims for RecogSpec types. It bridges Sort u carriers with APIs that expect Type u. CarrierType α is the abbreviation that sets CarrierType(α) := CarrierWrap(α), providing the target type for the equivalence.
proof idea
The definition builds the equivalence by setting the forward map to wrap a into ⟨a⟩, the inverse map to extract via .val, and both left and right inverses by reflexivity.
why it matters
This shim supports universe alignment inside the RecogSpec layer of the Recognition Science formalization. It enables practical interfacing between sorts and types without altering the underlying J-cost or phi-ladder structures. No downstream theorems are recorded, leaving its use as an internal bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.