CarrierType
plain-language theorem explainer
CarrierType supplies a universe shim that lifts a Sort u carrier into Type u via the CarrierWrap structure. Researchers maintaining polymorphic interfaces in the RecogSpec layer cite it when bridging sort-level data to type-based APIs. The definition is a direct one-line alias to CarrierWrap.
Claim. For a sort $α : Sort u$, the carrier type is the wrapper structure $CarrierWrap α$.
background
The RecogSpec.Universe module supplies small bridges for universe alignment and for interfacing Sort u carriers with APIs that expect Type u. CarrierWrap is the structure with a single field val : α that performs the lift from Sort u to Type u. This local convention lets downstream code treat carriers uniformly as inhabitants of Type u.
proof idea
The declaration is a one-line wrapper that aliases CarrierWrap α directly.
why it matters
CarrierType feeds the carrierEquiv equivalence, which constructs the isomorphism α ≃ CarrierType α by sending a to ⟨a⟩ and recovering the val field. It completes the minimal shim layer required for RecogSpec type specifications to remain universe-polymorphic without explicit level annotations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.