open import SOAS.Metatheory.Syntax

-- Initial (โ…€, ๐”›)-meta-algebra ๐•‹ ๐”› is the free โ…€-monoid on ๐”›
module SOAS.Metatheory.FreeMonoid {T : Set} (Syn : Syntax {T}) where

open Syntax Syn

open import SOAS.Common
open import SOAS.Families.Core {T}
open import SOAS.Context {T}
open import SOAS.Variable {T}
open import SOAS.Construction.Structure as Structure
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Coalgebra {T} as โ†’โ–ก ; open โ†’โ–ก.Sorted
import SOAS.Abstract.Box {T} as โ–ก ; open โ–ก.Sorted

open import Categories.Monad

open import SOAS.Abstract.Monoid

open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Monoid
open import SOAS.Coalgebraic.Strength
open import SOAS.Metatheory Syn


private
  variable
    ฮฑ ฮฒ : T
    ฮ“ ฮ” : Ctx

module _ (๐”› : Familyโ‚›) where
  open Theory ๐”›

  -- ๐•‹ is a ฮฃ-monoid
  ฮฃ๐•‹แต : ฮฃMon ๐•‹
  ฮฃ๐•‹แต =   record
    { แต = ๐•‹แต
    ; ๐‘Ž๐‘™๐‘” = ๐•’๐•๐•˜
    ; ฮผโŸจ๐‘Ž๐‘™๐‘”โŸฉ = ฮป{ {ฯƒ = ฯƒ} t โ†’ begin
          ๐•ค๐•ฆ๐•“ (๐•’๐•๐•˜ t) ฯƒ
      โ‰กโŸจ Substitution.๐•ฅโŸจ๐•’โŸฉ โŸฉ
          ๐•’๐•๐•˜ (str ๐•‹แดฎ ๐•‹ (โ…€โ‚ ๐•ค๐•ฆ๐•“ t) ฯƒ)
      โ‰กโŸจ cong ๐•’๐•๐•˜ (CoalgMon.str-eq ๐•‹แดน ๐•‹ โ…€:Str (โ…€โ‚ ๐•ค๐•ฆ๐•“ t) ฯƒ) โŸฉ
          ๐•’๐•๐•˜ (str (Mon.แดฎ ๐•‹แต) ๐•‹ (โ…€โ‚ ๐•ค๐•ฆ๐•“ t) ฯƒ)
      โˆŽ }
    } where open โ‰ก-Reasoning

  -- Given a โ…€-monoid โ„ณ and interpretation ฯ‰ : ๐”› โ‡พฬฃ โ„ณ,
  -- there is a unique homomorphic extension ๐•‹ ๐”› โ‡พฬฃ โ„ณ
  module FฮฃM {โ„ณ : Familyโ‚›}(ฮฃโ„ณแต : ฮฃMon โ„ณ) (ฯ‰ : ๐”› โ‡พฬฃ โ„ณ) where
    open ฮฃMon ฮฃโ„ณแต renaming (๐‘Ž๐‘™๐‘” to โ„ณ๐‘Ž๐‘™๐‘” ; แดฎ to โ„ณแดฎ ; แต to โ„ณแต) public
    private module โ„ณ = ฮฃMon ฮฃโ„ณแต

    -- Metavariable operator of โ„ณ using ฯ‰ and monoid multiplication, making
    -- โ„ณ into a meta-algebra
    ฯ‡ : ๐”› โ‡พฬฃ ใ€– โ„ณ , โ„ณ ใ€—
    ฯ‡ ๐”ช ฮต = ฮผ (ฯ‰ ๐”ช) ฮต

    โ„ณแตƒ : MetaAlg โ„ณ
    โ„ณแตƒ = record { ๐‘Ž๐‘™๐‘” = โ„ณ.๐‘Ž๐‘™๐‘” ; ๐‘ฃ๐‘Ž๐‘Ÿ = ฮท ; ๐‘š๐‘ฃ๐‘Ž๐‘Ÿ = ฯ‡ }

    open Semantics โ„ณแตƒ public renaming (๐•ค๐•–๐•ž to ๐•–๐•ฉ๐•ฅ)
    open MetaAlg โ„ณแตƒ
    open Coalgebraic ฮผแถœ

    -- Extension is pointed coalgebra hommorphism
    ๐•–๐•ฉ๐•ฅแต‡โ‡’ : Coalgโ‡’ ๐•‹แต‡ โ„ณ.แต‡ ๐•–๐•ฉ๐•ฅ
    ๐•–๐•ฉ๐•ฅแต‡โ‡’ = ๐•ค๐•–๐•žแต‡โ‡’ โ„ณ.แต‡ โ„ณแตƒ record
      { โŸจ๐‘Ž๐‘™๐‘”โŸฉ = ฮป{ {t = t} โ†’ dext (ฮป ฯ โ†’ begin
            ฮผ (๐‘Ž๐‘™๐‘” t) (ฮท โˆ˜ ฯ)
        โ‰กโŸจ ฮผโŸจ๐‘Ž๐‘™๐‘”โŸฉ t โŸฉ
            ๐‘Ž๐‘™๐‘” (str โ„ณ.แดฎ โ„ณ (โ…€โ‚ ฮผ t) (ฮท โˆ˜ ฯ))
        โ‰กโŸจ cong ๐‘Ž๐‘™๐‘” (str-natโ‚ (ฮทแดฎโ‡’ โ„ณแดฎ) (โ…€โ‚ โ„ณ.ฮผ t) ฯ) โŸฉ
            ๐‘Ž๐‘™๐‘” (str โ„แดฎ โ„ณ (โ…€.Fโ‚ (ฮป { h ฯ‚ โ†’ h (ฮป v โ†’ ฮท (ฯ‚ v)) }) (โ…€โ‚ โ„ณ.ฮผ t)) ฯ)
        โ‰กห˜โŸจ congr โ…€.homomorphism (ฮป - โ†’ ๐‘Ž๐‘™๐‘” (str โ„แดฎ โ„ณ - ฯ)) โŸฉ
            ๐‘Ž๐‘™๐‘” (str โ„แดฎ โ„ณ (โ…€.Fโ‚ (ฮป{ t ฯ โ†’ ฮผ t (ฮท โˆ˜ ฯ)}) t) ฯ)
        โˆŽ) }
      ; โŸจ๐‘ฃ๐‘Ž๐‘ŸโŸฉ = dextโ€ฒ โ„ณ.lunit
      ; โŸจ๐‘š๐‘ฃ๐‘Ž๐‘ŸโŸฉ = dextโ€ฒ โ„ณ.assoc
      } where open โ‰ก-Reasoning

    ๐•–๐•ฉ๐•ฅแดฎโ‡’ : Coalgโ‚šโ‡’ ๐•‹แดฎ โ„ณ.แดฎ ๐•–๐•ฉ๐•ฅ
    ๐•–๐•ฉ๐•ฅแดฎโ‡’ = record { แต‡โ‡’ = ๐•–๐•ฉ๐•ฅแต‡โ‡’ ; โŸจฮทโŸฉ = โŸจ๐•งโŸฉ }

    -- Extension is monoid homomorphims
    ฮผโˆ˜๐•–๐•ฉ๐•ฅ : MapEqโ‚ ๐•‹แดฎ โ„ณ.๐‘Ž๐‘™๐‘” (ฮป t ฯƒ โ†’ ๐•–๐•ฉ๐•ฅ (๐•ค๐•ฆ๐•“ t ฯƒ))
                           (ฮป t ฯƒ โ†’ ฮผ (๐•–๐•ฉ๐•ฅ t) (๐•–๐•ฉ๐•ฅ โˆ˜ ฯƒ))
    ฮผโˆ˜๐•–๐•ฉ๐•ฅ = record
      { ฯ† = ๐•–๐•ฉ๐•ฅ
      ; ฯ‡ = ฯ‡
      ; fโŸจ๐‘ฃโŸฉ = cong ๐•–๐•ฉ๐•ฅ Substitution.๐•ฅโŸจ๐•งโŸฉ
      ; fโŸจ๐‘šโŸฉ = trans (cong ๐•–๐•ฉ๐•ฅ Substitution.๐•ฅโŸจ๐•žโŸฉ) โŸจ๐•žโŸฉ
      ; fโŸจ๐‘ŽโŸฉ = ฮป{ {ฯƒ = ฯƒ}{t} โ†’ begin
            ๐•–๐•ฉ๐•ฅ (๐•ค๐•ฆ๐•“ (๐•’๐•๐•˜ t) ฯƒ)
        โ‰กโŸจ cong ๐•–๐•ฉ๐•ฅ Substitution.๐•ฅโŸจ๐•’โŸฉ โŸฉ
            ๐•–๐•ฉ๐•ฅ (๐•’๐•๐•˜ (str ๐•‹แดฎ ๐•‹ (โ…€โ‚ ๐•ค๐•ฆ๐•“ t) ฯƒ))
        โ‰กโŸจ โŸจ๐•’โŸฉ โŸฉ
            ๐‘Ž๐‘™๐‘” (โ…€โ‚ ๐•–๐•ฉ๐•ฅ (str ๐•‹แดฎ ๐•‹ (โ…€โ‚ ๐•ค๐•ฆ๐•“ t) ฯƒ))
        โ‰กห˜โŸจ cong ๐‘Ž๐‘™๐‘” (str-natโ‚‚ ๐•–๐•ฉ๐•ฅ (โ…€โ‚ ๐•ค๐•ฆ๐•“ t) ฯƒ) โŸฉ
            ๐‘Ž๐‘™๐‘” (str ๐•‹แดฎ โ„ณ (โ…€.Fโ‚ (ฮป { h ฯ‚ โ†’ ๐•–๐•ฉ๐•ฅ (h ฯ‚) }) (โ…€โ‚ ๐•ค๐•ฆ๐•“ t)) ฯƒ)
        โ‰กห˜โŸจ congr โ…€.homomorphism (ฮป - โ†’ ๐‘Ž๐‘™๐‘” (str ๐•‹แดฎ โ„ณ - ฯƒ))  โŸฉ
            ๐‘Ž๐‘™๐‘” (str ๐•‹แดฎ โ„ณ (โ…€โ‚ (ฮป{ t ฯƒ โ†’ ๐•–๐•ฉ๐•ฅ (๐•ค๐•ฆ๐•“ t ฯƒ)}) t) ฯƒ)
        โˆŽ }
      ; gโŸจ๐‘ฃโŸฉ = trans (ฮผโ‰ˆโ‚ โŸจ๐•งโŸฉ) (Mon.lunit โ„ณ.แต)
      ; gโŸจ๐‘šโŸฉ = trans (ฮผโ‰ˆโ‚ โŸจ๐•žโŸฉ) (Mon.assoc โ„ณ.แต)
      ; gโŸจ๐‘ŽโŸฉ = ฮป{ {ฯƒ = ฯƒ}{t} โ†’ begin
            ฮผ (๐•–๐•ฉ๐•ฅ (๐•’๐•๐•˜ t)) (๐•–๐•ฉ๐•ฅ โˆ˜ ฯƒ)
        โ‰กโŸจ ฮผโ‰ˆโ‚ โŸจ๐•’โŸฉ โŸฉ
            ฮผ (๐‘Ž๐‘™๐‘” (โ…€โ‚ ๐•–๐•ฉ๐•ฅ t)) (๐•–๐•ฉ๐•ฅ โˆ˜ ฯƒ)
        โ‰กโŸจ ฮผโŸจ๐‘Ž๐‘™๐‘”โŸฉ _ โŸฉ
            ๐‘Ž๐‘™๐‘” (str โ„ณแดฎ โ„ณ (โ…€โ‚ ฮผ (โ…€โ‚ ๐•–๐•ฉ๐•ฅ t)) (๐•–๐•ฉ๐•ฅ โˆ˜ ฯƒ))
        โ‰กห˜โŸจ congr โ…€.homomorphism (ฮป - โ†’ ๐‘Ž๐‘™๐‘” (str โ„ณแดฎ โ„ณ - (๐•–๐•ฉ๐•ฅ โˆ˜ ฯƒ))) โŸฉ
            ๐‘Ž๐‘™๐‘” (str โ„ณแดฎ โ„ณ (โ…€โ‚ (ฮผ โˆ˜ ๐•–๐•ฉ๐•ฅ) t) (๐•–๐•ฉ๐•ฅ โˆ˜ ฯƒ))
        โ‰กโŸจ cong ๐‘Ž๐‘™๐‘” (str-natโ‚ ๐•–๐•ฉ๐•ฅแดฎโ‡’ ((โ…€โ‚ (ฮผ โˆ˜ ๐•–๐•ฉ๐•ฅ) t)) ฯƒ) โŸฉ
            ๐‘Ž๐‘™๐‘” (str ๐•‹แดฎ โ„ณ (โ…€.Fโ‚ (ฮป { hโ€ฒ ฯ‚ โ†’ hโ€ฒ (๐•–๐•ฉ๐•ฅ โˆ˜ ฯ‚) }) (โ…€โ‚ (ฮผ โˆ˜ ๐•–๐•ฉ๐•ฅ) t)) ฯƒ)
        โ‰กห˜โŸจ congr โ…€.homomorphism (ฮป - โ†’ โ„ณ๐‘Ž๐‘™๐‘” (str ๐•‹แดฎ โ„ณ - ฯƒ))  โŸฉ
            ๐‘Ž๐‘™๐‘” (str ๐•‹แดฎ โ„ณ (โ…€โ‚ (ฮป{ t ฯƒ โ†’ ฮผ (๐•–๐•ฉ๐•ฅ t) (๐•–๐•ฉ๐•ฅ โˆ˜ ฯƒ)}) t) ฯƒ)
        โˆŽ }
      } where open โ‰ก-Reasoning


    ๐•–๐•ฉ๐•ฅแตโ‡’ : ฮฃMonโ‡’ ฮฃ๐•‹แต ฮฃโ„ณแต ๐•–๐•ฉ๐•ฅ
    ๐•–๐•ฉ๐•ฅแตโ‡’ = record { แตโ‡’ = record
      { โŸจฮทโŸฉ = โŸจ๐•งโŸฉ
      ; โŸจฮผโŸฉ = ฮป{ {t = t} โ†’ MapEqโ‚.โ‰ˆ ฮผโˆ˜๐•–๐•ฉ๐•ฅ t } }
      ; โŸจ๐‘Ž๐‘™๐‘”โŸฉ = โŸจ๐•’โŸฉ }

    module ๐•–๐•ฉ๐•ฅแตโ‡’ = ฮฃMonโ‡’ ๐•–๐•ฉ๐•ฅแตโ‡’

    -- Interpretation map is equal to any homomorphism that factors through ๐”› โ‡พ โ„ณ
    module _ {g : ๐•‹ โ‡พฬฃ โ„ณ}
             (gแตโ‡’ : ฮฃMonโ‡’ ฮฃ๐•‹แต ฮฃโ„ณแต g)
             (p : โˆ€{ฮฑ ฮ }{๐”ช : ๐”› ฮฑ ฮ } โ†’ g (๐•ž๐•ง๐•’๐•ฃ ๐”ช ๐•ง๐•’๐•ฃ) โ‰ก ฯ‰ ๐”ช) where
      open ฮฃMonโ‡’ gแตโ‡’ renaming (โŸจ๐‘Ž๐‘™๐‘”โŸฉ to gโŸจ๐‘Ž๐‘™๐‘”โŸฉ)

      gแตƒโ‡’ : MetaAlgโ‡’ ๐•‹แตƒ โ„ณแตƒ g
      gแตƒโ‡’ = record
        { โŸจ๐‘Ž๐‘™๐‘”โŸฉ = gโŸจ๐‘Ž๐‘™๐‘”โŸฉ
        ; โŸจ๐‘ฃ๐‘Ž๐‘ŸโŸฉ = โŸจฮทโŸฉ
        ; โŸจ๐‘š๐‘ฃ๐‘Ž๐‘ŸโŸฉ = ฮป{ {๐”ช = ๐”ช}{ฮต} โ†’ begin
            g (๐•ž๐•ง๐•’๐•ฃ ๐”ช ฮต)                     โ‰กห˜โŸจ cong g (cong (๐•ž๐•ง๐•’๐•ฃ ๐”ช) (dextโ€ฒ Substitution.๐•ฅโŸจ๐•งโŸฉ)) โŸฉ
            g (๐•ž๐•ง๐•’๐•ฃ ๐”ช (ฮป v โ†’ ๐•ค๐•ฆ๐•“ (๐•ง๐•’๐•ฃ v) ฮต))  โ‰กห˜โŸจ cong g Substitution.๐•ฅโŸจ๐•žโŸฉ โŸฉ
            g (๐•ค๐•ฆ๐•“ (๐•ž๐•ง๐•’๐•ฃ ๐”ช ๐•ง๐•’๐•ฃ) ฮต)            โ‰กโŸจ โŸจฮผโŸฉ โŸฉ
            ฮผ (g (๐•ž๐•ง๐•’๐•ฃ ๐”ช ๐•ง๐•’๐•ฃ)) (g โˆ˜ ฮต)        โ‰กโŸจ ฮผโ‰ˆโ‚ p โŸฉ
            ฮผ (ฯ‰ ๐”ช) (ฮป x โ†’ g (ฮต x))          โˆŽ  }
        } where open โ‰ก-Reasoning

      ๐•–๐•ฉ๐•ฅแต! : {ฮฑ : T}{ฮ“ : Ctx}(t : ๐•‹ ฮฑ ฮ“) โ†’ ๐•–๐•ฉ๐•ฅ t โ‰ก g t
      ๐•–๐•ฉ๐•ฅแต! = ๐•ค๐•–๐•ž! gแตƒโ‡’

-- Free ฮฃ-monoid functor
Famโ‚›โ†’ฮฃMon :  Familyโ‚› โ†’ ฮฃMonoid
Famโ‚›โ†’ฮฃMon ๐”› = Theory.๐•‹ ๐”› โ‹‰ (ฮฃ๐•‹แต ๐”›)

open ฮฃMonoidStructure.Free

Free-ฮฃMon-Mapping : FreeฮฃMonoid.FreeMapping Famโ‚›โ†’ฮฃMon
Free-ฮฃMon-Mapping = record
  { embed = ฮป {๐”›} ๐”ช โ†’ let open Theory ๐”› in ๐•ž๐•ง๐•’๐•ฃ ๐”ช ๐•ง๐•’๐•ฃ
  ; univ = ฮป{ ๐”› (โ„ณ โ‹‰ ฮฃโ„ณแต) ฯ‰ โ†’ let open FฮฃM ๐”› ฮฃโ„ณแต ฯ‰ in record
    { extend = ๐•–๐•ฉ๐•ฅ โ‹‰ ๐•–๐•ฉ๐•ฅแตโ‡’
    ; factor = trans โŸจ๐•žโŸฉ (trans (ฮผโ‰ˆโ‚‚ โŸจ๐•งโŸฉ) runit)
    ; unique = ฮป{ (g โ‹‰ gแตโ‡’) p {x = t} โ†’ sym (๐•–๐•ฉ๐•ฅแต! gแตโ‡’ p t) } }}
  }

Free:๐”ฝamโ‚›โŸถฮฃ๐•„on : Functor ๐”ฝamiliesโ‚› ฮฃ๐•„onoids
Free:๐”ฝamโ‚›โŸถฮฃ๐•„on = FreeฮฃMonoid.FreeMapping.Free Free-ฮฃMon-Mapping

-- ฮฃ-monoid monad on families
ฮฃMon:Monad : Monad ๐”ฝamiliesโ‚›
ฮฃMon:Monad = FreeฮฃMonoid.FreeMapping.FreeMonad Free-ฮฃMon-Mapping

๐•‹F : Functor ๐”ฝamiliesโ‚› ๐”ฝamiliesโ‚›
๐•‹F = Monad.F ฮฃMon:Monad

open Theory
open Monad ฮฃMon:Monad

-- Functorial action of ๐•‹
๐•‹โ‚ : {๐”› ๐”œ : Familyโ‚›} โ†’ (๐”› โ‡พฬฃ ๐”œ) โ†’ ๐•‹ ๐”› โ‡พฬฃ ๐•‹ ๐”œ
๐•‹โ‚ f t = Functor.โ‚ ๐•‹F f t

-- Functorial action preserves variables
๐•‹โ‚โˆ˜๐•ง๐•’๐•ฃ : {๐”› ๐”œ : Familyโ‚›}(f : ๐”› โ‡พฬฃ ๐”œ)(v : โ„ ฮฑ ฮ“)
       โ†’ ๐•‹โ‚ f (๐•ง๐•’๐•ฃ ๐”› v) โ‰ก ๐•ง๐•’๐•ฃ ๐”œ v
๐•‹โ‚โˆ˜๐•ง๐•’๐•ฃ {๐”› = ๐”›}{๐”œ} f v = FฮฃM.โŸจ๐•งโŸฉ ๐”› (ฮฃ๐•‹แต ๐”œ) (ฮป ๐”ช โ†’ ๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (๐•ง๐•’๐•ฃ ๐”œ))

-- Functorial action preserves metavariables
๐•‹โ‚โˆ˜๐•ž๐•ง๐•’๐•ฃ : {๐”› ๐”œ : Familyโ‚›}(f : ๐”› โ‡พฬฃ ๐”œ)(๐”ช : ๐”› ฮฑ ฮ“)(ฮต : ฮ“ ~[ ๐•‹ ๐”› ]โ† ฮ”)
       โ†’ ๐•‹โ‚ f (๐•ž๐•ง๐•’๐•ฃ ๐”› ๐”ช ฮต) โ‰ก ๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (๐•‹โ‚ f โˆ˜ ฮต)
๐•‹โ‚โˆ˜๐•ž๐•ง๐•’๐•ฃ {๐”› = ๐”›}{๐”œ} f ๐”ช ฮต = begin
      ๐•‹โ‚ f (๐•ž๐•ง๐•’๐•ฃ ๐”› ๐”ช ฮต)
  โ‰กโŸจโŸฉ
      FฮฃM.๐•–๐•ฉ๐•ฅ ๐”› (ฮฃ๐•‹แต ๐”œ) (ฮป ๐”ช โ†’ ๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (๐•ง๐•’๐•ฃ ๐”œ)) (๐•ž๐•ง๐•’๐•ฃ ๐”› ๐”ช ฮต)
  โ‰กโŸจ FฮฃM.โŸจ๐•žโŸฉ ๐”› (ฮฃ๐•‹แต ๐”œ) (ฮป ๐”ช โ†’ ๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (๐•ง๐•’๐•ฃ ๐”œ)) โŸฉ
      ๐•ค๐•ฆ๐•“ ๐”œ (๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (๐•ง๐•’๐•ฃ ๐”œ)) (๐•‹โ‚ f โˆ˜ ฮต)
  โ‰กโŸจ Substitution.๐•ฅโŸจ๐•žโŸฉ ๐”œ โŸฉ
      ๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (ฮป ๐”ซ โ†’ ๐•ค๐•ฆ๐•“ ๐”œ (๐•ง๐•’๐•ฃ ๐”œ ๐”ซ) (๐•‹โ‚ f โˆ˜ ฮต))
  โ‰กโŸจ cong (๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช)) (dext (ฮป ๐”ซ โ†’ lunit ๐”œ)) โŸฉ
      ๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (๐•‹โ‚ f โˆ˜ ฮต)
  โˆŽ where open โ‰ก-Reasoning

-- Corollary fo the above two
๐•‹โ‚โˆ˜๐•ž๐•ง๐•’๐•ฃ[๐•ง๐•’๐•ฃ] : {๐”› ๐”œ : Familyโ‚›}(f : ๐”› โ‡พฬฃ ๐”œ)(๐”ช : ๐”› ฮฑ ฮ“)(ฯ : ฮ“ โ† ฮ”)
       โ†’ ๐•‹โ‚ f (๐•ž๐•ง๐•’๐•ฃ ๐”› ๐”ช (๐•ง๐•’๐•ฃ ๐”› โˆ˜ ฯ)) โ‰ก ๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (๐•ง๐•’๐•ฃ ๐”œ โˆ˜ ฯ)
๐•‹โ‚โˆ˜๐•ž๐•ง๐•’๐•ฃ[๐•ง๐•’๐•ฃ] {๐”› = ๐”›}{๐”œ} f ๐”ช ฯ = begin
      ๐•‹โ‚ f (๐•ž๐•ง๐•’๐•ฃ ๐”› ๐”ช (๐•ง๐•’๐•ฃ ๐”› โˆ˜ ฯ))
  โ‰กโŸจ ๐•‹โ‚โˆ˜๐•ž๐•ง๐•’๐•ฃ f ๐”ช (๐•ง๐•’๐•ฃ ๐”› โˆ˜ ฯ) โŸฉ
      ๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (๐•‹โ‚ f โˆ˜ ๐•ง๐•’๐•ฃ ๐”› โˆ˜ ฯ)
  โ‰กโŸจ cong (๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช)) (dext ฮป v โ†’ ๐•‹โ‚โˆ˜๐•ง๐•’๐•ฃ f (ฯ v)) โŸฉ
      ๐•ž๐•ง๐•’๐•ฃ ๐”œ (f ๐”ช) (๐•ง๐•’๐•ฃ ๐”œ โˆ˜ ฯ)
  โˆŽ where open โ‰ก-Reasoning