CarrierWrap
plain-language theorem explainer
CarrierWrap defines a minimal structure that lifts a value from Sort u into Type u. It is cited by type definitions in RecogSpec that must satisfy APIs expecting Type u while preserving the original carrier. The definition is a direct single-field structure with no additional axioms or reductions.
Claim. Given a sort $α : Sort u$, the structure $CarrierWrap α$ is a type in $Type u$ with a single field $val : α$.
background
The module RecogSpec.Universe supplies small bridges for universe alignment between Sort u carriers and Type u contexts. CarrierWrap is the concrete structure that performs this lift so that values originally declared in Sort u can be used where Type u is required. No upstream lemmas are involved; the definition stands alone as a universe shim.
proof idea
Direct structure definition that introduces a single constructor field val of type α.
why it matters
CarrierWrap is the immediate definition underlying the abbrev CarrierType, which is the entry point for RecogSpec types that must cross universe boundaries. It supplies the minimal technical device needed to keep carrier types compatible with downstream APIs while staying inside the Recognition Science type hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.