question about rfl

Stream: lean4

[MangoIV]

This rfl:
https://git.sr.ht/~mangoiv/leff/tree/4945e83c0d40965f3c756e8271c6cdaaffd448aa/item/src/Leff/Control/Algebra.lean#L45

has the following goal:

⊢
  Handler.handler handler₁ (σ₂ α) (Handler.handler handler₂ α <$> pure <$> p) =
  Handler.handler handler₁ (σ₂ α) (Handler.handler handler₂ α <$> Functor.map pure <$> p)

for me those somehow don't look the same, why can rfl see those are the same? Or is this a display issue?

[Siddharth Bhat]

If we simplify the core of the equality, we see that we have:

def core [Functor σ₁] [Functor σ₂] [LawfulFunctor σ₁]
  [LawfulFunctor σ₂][Monad l] [LawfulMonad l]
  (p : Functor.Comp σ₁ σ₂ α) :
    (pure (f := l) <$> p) = Functor.map (pure (f := l)) <$> p :=  rfl

The left-hand-side is fmapping pure to create Functor.Comp σ₁ σ₂ (l α) by lifting the pure over the _entire_ functor Functor.Comp σ₁ σ₂ .

the right-hand-side is using a "map of map" (see that there are two maps, one from Functor.map, and another from <$>, to lift pure through the _two layers_ of functors, one from σ₂ and one from σ₁. This is possible, because the type (Functor.Comp σ₁ σ₂) α is defeq to σ₁ (σ₂ (α)).

[MangoIV]

yeah so it's kinda luck that i saw the type to be Comp sigma_1 sigma_2 instead of something else cause then I'd sit on it still :D Thank you for investigating!

[Siddharth Bhat]

Slightly cleaned up version:

/-- The Functor.comp applied to the argument
  is definitionally equal to the functors applied to the argument -/
def comp_eq : Functor.Comp f g a = f (g a) := rfl

/--
Manually applied version of the LHS and RHS.
-/
def core [S1: Functor σ₁] [S2: Functor σ₂] [ML : Monad l]
  (p : Functor.Comp σ₁ σ₂ α) :
    (Functor.Comp.map ML.pure p) =
    S1.map (S2.map ML.pure) p :=  rfl