Lean4
/-- Expressions for 2-morphisms. -/
inductive Mor₂ : Type where/-- The expression for `Iso.hom`. -/
| isoHom (e : Expr) (isoLift : IsoLift) (iso : Mor₂Iso) : Mor₂/-- The expression for `Iso.inv`. -/
| isoInv (e : Expr) (isoLift : IsoLift) (iso : Mor₂Iso) : Mor₂/-- The expression for the identity `𝟙 f`. -/
| id (e : Expr) (isoLift : IsoLift) (f : Mor₁) : Mor₂/-- The expression for the composition `η ≫ θ`. -/
| comp (e : Expr) (isoLift? : Option IsoLift) (f g h : Mor₁) (η θ : Mor₂) : Mor₂/--
The expression for the left whiskering `f ◁ η` with `η : g ⟶ h`. -/
| whiskerLeft (e : Expr) (isoLift? : Option IsoLift) (f g h : Mor₁) (η : Mor₂) : Mor₂/--
The expression for the right whiskering `η ▷ h` with `η : f ⟶ g`. -/
| whiskerRight (e : Expr) (isoLift? : Option IsoLift) (f g : Mor₁) (η : Mor₂) (h : Mor₁) : Mor₂/--
The expression for the horizontal composition `η ◫ θ` with `η : f₁ ⟶ g₁` and `θ : f₂ ⟶ g₂`. -/
| horizontalComp (e : Expr) (isoLift? : Option IsoLift) (f₁ g₁ f₂ g₂ : Mor₁) (η θ : Mor₂) : Mor₂/--
The expression for the coherence composition `η ⊗≫ θ := η ≫ α ≫ θ` with `η : f ⟶ g`
and `θ : h ⟶ i`. -/
| coherenceComp (e : Expr) (isoLift? : Option IsoLift) (f g h i : Mor₁) (α : CoherenceHom) (η θ : Mor₂) : Mor₂/--
The expression for an atomic non-structural 2-morphism. -/
| of (η : Atom) : Mor₂
deriving Inhabited
