`deconstructAssociator`🔗

Definition

Deconstruct an associator [inverse] morphism.

def

deconstructAssociator (e : Lean.Expr) (eLvl : Lean.Level) (hom : Bool) :
  Lean.MetaM (Lean.Expr × Lean.Expr)
deconstructAssociator (e : Lean.Expr)
  (eLvl : Lean.Level) (hom : Bool) :
  Lean.MetaM (Lean.Expr × Lean.Expr)

Code

def deconstructAssociator (e : Expr) (eLvl : Level) (hom : Bool) : MetaM (Expr × Expr) := do
  let args := e.getAppArgs
  let SZ := args[args.size - 1]!
  let SY := args[args.size - 2]!
  let SX := args[args.size - 3]!
  let Z ← getTypeFromSFinKer SZ
  let Y ← getTypeFromSFinKer SY
  let X ← getTypeFromSFinKer SX
  let (Z₀, z₀Lvl) ← getOriginalType Z
  let (Y₀, y₀Lvl) ← getOriginalType Y
  let (X₀, x₀Lvl) ← getOriginalType X
  let ez₀ ← constructMeasurableEquiv Z₀ z₀Lvl eLvl
  let ey₀ ← constructMeasurableEquiv Y₀ y₀Lvl eLvl
  let ex₀ ← constructMeasurableEquiv X₀ x₀Lvl eLvl
  let associator_const := mkConst
    (if hom then ``Kernel.associator_hom else ``Kernel.associator_inv)
    [eLvl, eLvl, eLvl, x₀Lvl, y₀Lvl, z₀Lvl, eLvl]
  let associator_proof_eq ← mkAppM' associator_const
    #[SX, SY, SZ, ← idME X, ← idME Y, ← idME Z, ex₀, ey₀, ez₀]
  return (← getKernelRHSEqProofType associator_proof_eq, associator_proof_eq)

Actions: Source · Open Issue

Meaning last changed in v4.34.0-rc2-1-g439785b (2026-08-23).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 5 project declarations, 111 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

deconstructAssociator🔗

`deconstructAssociator`🔗