IndisputableMonolith.RecogSpec.Universe

   1import Mathlib
   2
   3/-!
   4Universe helpers and shims for RecogSpec types.
   5
   6This file provides small bridges for universe alignment and for interfacing
   7`Sort u` carriers with APIs that expect `Type u`.
   8-/
   9
  10namespace RecogSpec
  11
  12universe u
  13
  14/-!
  15`CarrierType` and `carrierEquiv` present a canonical way to use `Type u`
  16when an external API requires it, starting from an arbitrary `Sort u` carrier.
  17-/
  18
  19structure CarrierWrap (α : Sort u) : Type u where
  20  val : α
  21
  22abbrev CarrierType (α : Sort u) : Type u := CarrierWrap α
  23
  24@[simp] def carrierEquiv (α : Sort u) : α ≃ CarrierType α :=
  25{ toFun := fun a => ⟨a⟩,
  26  invFun := fun w => w.val,
  27  left_inv := by intro a; rfl,
  28  right_inv := by intro w; cases w; rfl }
  29
  30end RecogSpec
  31