{-# OPTIONS --without-K  --cubical-compatible #-}

open import common
open import inductive-repair.indspec
open import inductive-repair.config

{-
    W-type configurations: every signature embeds into a
    single-constructor W-type signature (shape + positions), and
    every `Config` induces a `WTypeConfig` (`allConfigWTypeConfig`).
    The core is the polynomial view of `Args` (`convert` /
    `unconvert`) with its triangle identity.
-}
module inductive-repair.wtype-config {ℓ : Level} where
    {-
        The single constructor for a W-type has one nonrec arg and one rec arg.
    -}
    WTypeArity : {ℓ : Level} → (A : Type ℓ) → (B : A → Type ℓ) → ⊤ {ℓ} → ConstrArity {ℓ}
    WTypeArity A B _ = Nonrec A (λ a → Rec (B a) Done)

    WTypeSignature : {ℓ : Level} → (A : Type ℓ) → (B : A → Type ℓ) → Signature
    WTypeSignature _ _ .Signature.Op = ⊤
    WTypeSignature {ℓ} A B .Signature.arity = WTypeArity {ℓ} A B

    WTypeIndAlg : {ℓ : Level} → (A : Type ℓ) → (B : A → Type ℓ) → (C : Type ℓ) → Type (lsuc ℓ)
    WTypeIndAlg {ℓ} A B C = IndAlg (WTypeSignature {ℓ} A B) C

    WTypeConfig : {ℓ : Level} → (A : Type ℓ) → (B : A → Type ℓ) → (C D : Type ℓ) → Type (lsuc ℓ)
    WTypeConfig {ℓ} A B C D = Config (WTypeSignature {ℓ} A B) C D

    module _ {sig : Signature {ℓ}} where
        arity = Signature.arity sig
        Op = Signature.Op sig

        {-
            Positions of the recursive arguments inside a shape.

            A "shape" is just `Args` with the carrier replaced by `⊤`;
            it forgets the recursive functions and keeps the nonrec data.
        -}
        recPos : (cs : ConstrArity {ℓ}) → Args cs (⊤ {ℓ}) → Type ℓ
        recPos Done         _          = ⊥
        recPos (Nonrec A k) (a , s)    = recPos (k a) s
        recPos (Rec D cs)   (_ , s)    = D ⊎ recPos cs s

        {-
            Sum eliminator used as `β-emb`'s position function. Factored to
            module scope so any term that builds the same sum function (in
            β-emb output, in convert (Rec D cs), in path proofs against it)
            references the same name. Agda treats `λ where`s at distinct
            source locations as intensionally distinct, which would
            otherwise block definitional equalities.
        -}
        β-emb-pos : {D X C : Type ℓ} (r : D → C) (q : X → C) → D ⊎ X → C
        β-emb-pos r q (inl d) = r d
        β-emb-pos r q (inr x) = q x

        {-
            Embed a `Σ Shape (Pos → C)` for `cs` into one for `Rec D cs` by
            providing the rec function `r : D → C`.
        -}
        β-emb : (D : Type ℓ) (cs : ConstrArity {ℓ}) {C : Type ℓ} → (D → C) →
                Σ (Args cs (⊤ {ℓ})) (λ s' → recPos cs s' → C) →
                Σ (Args (Rec D cs) (⊤ {ℓ})) (λ s' → recPos (Rec D cs) s' → C)
        β-emb D cs r q = (((λ _ → tt) , fst q) , β-emb-pos r (snd q))

        {-
            Polynomial view: `Args cs C` is equivalent to
            `Σ (Shape) (λ s → recPos cs s → C)` where `Shape = Args cs ⊤`.
            We provide `convert` and `unconvert` as that equivalence, with
            `unconvert ∘ convert ≡ id` holding definitionally.
        -}
        convert : (cs : ConstrArity {ℓ}) {C : Type ℓ} → Args cs C →
                  Σ (Args cs (⊤ {ℓ})) (λ s → recPos cs s → C)
        convert Done         _          = (tt , λ ())
        convert (Nonrec A k) (a , args) =
            let (s , p) = convert (k a) args in ((a , s) , p)
        convert (Rec D cs)   (r , args) = β-emb D cs r (convert cs args)

        unconvert : (cs : ConstrArity {ℓ}) {C : Type ℓ} →
                    Σ (Args cs (⊤ {ℓ})) (λ s → recPos cs s → C) →
                    Args cs C
        unconvert Done         _              = tt
        unconvert (Nonrec A k) ((a , s) , p)  = (a , unconvert (k a) (s , p))
        unconvert (Rec D cs)   ((_ , s) , p)  =
            ((λ d → p (inl d)) , unconvert cs (s , λ z → p (inr z)))

        {-
            `unconvert ∘ convert = id` holds definitionally — pattern matching
            on `cs` lets `refl` work in every case (using Agda's η for
            functions and for `⊤`).
        -}
        unconvert-convert : {C : Type ℓ} (cs : ConstrArity {ℓ}) (args : Args cs C) →
                            unconvert cs (convert cs args) ≡ args
        unconvert-convert Done         _          = refl
        unconvert-convert (Nonrec A k) (a , args) = ap (λ z → (a , z)) (unconvert-convert (k a) args)
        unconvert-convert (Rec D cs)   (r , args) = ap (λ z → (r , z)) (unconvert-convert cs args)

        {-
            Pointwise refl: `β-emb-pos (λ d → p (inl d)) (λ z → p (inr z))`
            agrees with `p` at every input — by the constructor cases.
            (This is sum-η spelled out by hand. Factored so γ-fix and the
            triangle's `ap`-proof reference the same homotopy.)
        -}
        pwr-of : {D : Type ℓ} (cs : ConstrArity {ℓ}) {C : Type ℓ}
                 {s : Args cs (⊤ {ℓ})}
                 (p : recPos (Rec D cs) ((λ _ → tt) , s) → C) →
                 (x : D ⊎ recPos cs s) →
                 β-emb-pos (λ d → p (inl d)) (λ z → p (inr z)) x ≡ p x
        pwr-of cs p (inl d) = refl
        pwr-of cs p (inr z) = refl

        {-
            The "γ" path for the Rec case of `convert-unconvert`: bridges
            the β-emb-image to the original Σ-pair via the pointwise-refl
            funext. Factored to module scope so `triangle` references the
            same path that `convert-unconvert (Rec D cs)` produces.
        -}
        γ-fix : (D : Type ℓ) (cs : ConstrArity {ℓ}) {C : Type ℓ}
                (s : Args cs (⊤ {ℓ}))
                (p : recPos (Rec D cs) ((λ _ → tt) , s) → C) →
                β-emb D cs (λ d → p (inl d)) (s , λ z → p (inr z))
                ≡ (((λ _ → tt) , s) , p)
        γ-fix D cs s p = Σ-≡-intro refl (ext (pwr-of cs p))

        {-
            `convert ∘ unconvert = id` holds up to funext on positions
            (the shape part matches definitionally via η-on-⊤).
        -}
        convert-unconvert : {C : Type ℓ} (cs : ConstrArity {ℓ})
                            (sp : Σ (Args cs (⊤ {ℓ})) (λ s → recPos cs s → C)) →
                            convert cs (unconvert cs sp) ≡ sp
        convert-unconvert Done         (tt , p)         = Σ-≡-intro refl (ext (λ ()))
        convert-unconvert (Nonrec A k) ((a , s) , p)    =
            ap (λ q → ((a , fst q) , snd q)) (convert-unconvert (k a) (s , p))
        convert-unconvert (Rec D cs)   ((_ , s) , p)    =
              ap (β-emb D cs (λ d → p (inl d))) (convert-unconvert cs (s , λ z → p (inr z)))
            • γ-fix D cs s p

        {-
            Naturality of `unconvert` in the carrier: mapping a function
            over the positions and then unconverting agrees with
            unconverting first and mapping over the recursive children.
        -}
        unconvert-mapArgs : (cs : ConstrArity {ℓ}) {C D : Type ℓ} (h : C → D)
                            (sp : Σ (Args cs (⊤ {ℓ})) (λ s → recPos cs s → C)) →
                            unconvert cs (fst sp , h ∘ snd sp)
                              ≡ mapArgs cs h (unconvert cs sp)
        unconvert-mapArgs Done         h _              = refl
        unconvert-mapArgs (Nonrec A k) h ((a , s) , p)  =
            ap (λ z → (a , z)) (unconvert-mapArgs (k a) h (s , p))
        unconvert-mapArgs (Rec D cs)   h ((_ , s) , p)  =
            ap (λ z → ((λ d → h (p (inl d))) , z))
               (unconvert-mapArgs cs h (s , (λ z → p (inr z))))

        {-
            Lift convertIH along the polynomial view: turn per-constructor
            IH on `Args` into IH on the W-type (single sum function
            on positions).
        -}
        convertIH : (cs : ConstrArity {ℓ}) {C : Type ℓ} {motive : C → Type ℓ}
                    (args : Args cs C) →
                    IHs cs motive args →
                    (z : recPos cs (fst (convert cs args))) →
                    motive (snd (convert cs args) z)
        convertIH Done         _          _                  ()
        convertIH (Nonrec A k) (a , args) ih                 z       = convertIH (k a) args ih z
        convertIH (Rec D cs)   (r , args) (ih_h , ih_t) (inl d)      = ih_h d
        convertIH (Rec D cs)   (r , args) (ih_h , ih_t) (inr z)      = convertIH cs args ih_t z

        {-
            Triangle identity / half-adjoint coherence: the path produced by
            `unconvert-convert` at `unconvert cs sp` agrees with the image of
            `convert-unconvert cs sp` under `unconvert cs`.

            Proved by structural induction on `cs`. With the `β-emb` refactor
            above, `convert (Rec D cs) ∘ unconvert (Rec D cs)` lands in
            β-emb-image definitionally, so the `Rec` case's path through
            `convert-unconvert (Rec D cs)` has only two segments — β-step
            and γ-path — and the chain to `LHS` factors through the same
            composition (via function-η and Σ-η on the inner projections).
            The remaining work is `ap U γ-path ≡ refl`, proved below.
        -}
        triangle : {C : Type ℓ} (cs : ConstrArity {ℓ})
                   (sp : Σ (Args cs (⊤ {ℓ})) (λ s → recPos cs s → C)) →
                   unconvert-convert cs (unconvert cs sp)
                   ≡ ap (unconvert cs) (convert-unconvert cs sp)
        triangle Done         (tt , p)      = ! (ap-const (Σ-≡-intro refl (ext (λ ()))))
        triangle (Nonrec A k) ((a , s) , p) =
            ap (ap (λ z → (a , z))) (triangle (k a) (s , p))
            • ! (ap-∘ (convert-unconvert (k a) (s , p)))
            • ap-∘ (convert-unconvert (k a) (s , p))
        triangle {C} (Rec D cs)   ((shape0 , s) , p) =
              ap (ap (λ z → ((λ d → p (inl d)) , z)))
                 (triangle cs (s , λ z → p (inr z)))
            • ! (ap-∘ (convert-unconvert cs (s , λ z → p (inr z))))
            • ap-∘ {f = unconvert (Rec D cs)} {g = β-emb D cs (λ d → p (inl d))}
                   (convert-unconvert cs (s , λ z → p (inr z)))
            • ! •unitr
            • ap (ap (unconvert (Rec D cs)) β-step •_) (! ap-γ-refl)
            • ! (ap-• (unconvert (Rec D cs)) β-step γ-path)
          where
            β-step : β-emb D cs (λ d → p (inl d))
                       (convert cs (unconvert cs (s , λ z → p (inr z))))
                   ≡ β-emb D cs (λ d → p (inl d)) (s , λ z → p (inr z))
            β-step = ap (β-emb D cs (λ d → p (inl d)))
                        (convert-unconvert cs (s , λ z → p (inr z)))

            γ-path : β-emb D cs (λ d → p (inl d)) (s , λ z → p (inr z))
                   ≡ (((λ _ → tt) , s) , p)
            γ-path = γ-fix D cs s p

            {- Decomposition: ap-on-precomp-inl is pwr-on-inl ext → refl. -}
            ap-precomp-inl-refl :
                ap (λ v → λ d → v (inl d)) (ext (pwr-of cs p)) ≡ refl
            ap-precomp-inl-refl =
                precomp-ext inl (pwr-of cs p)
              • ! funext-refl

            ap-snd-side-refl :
                ap (λ v → unconvert cs (s , λ z → v (inr z))) (ext (pwr-of cs p))
                ≡ refl
            ap-snd-side-refl =
                ap-∘ (ext (pwr-of cs p))
              • ap (ap (unconvert cs))
                   ( ap-∘ (ext (pwr-of cs p))
                   • ap (ap (λ q → (s , q)))
                        ( precomp-ext inr (pwr-of cs p)
                        • ! funext-refl))

            {- J-style collapse for non-dependent Σ (product): when both
               components are propositionally refl, the Σ-≡-intro is refl. -}
            collapse-Σ-product : {A : Type ℓ} {B : Type ℓ}
                                 {a : A} {b : B}
                                 {x : a ≡ a} {y : b ≡ b}
                                 (q1 : x ≡ refl) (q2 : y ≡ refl) →
                                 Σ-≡-intro {B = λ _ → B} x (tptConst x b • y) ≡ refl
            collapse-Σ-product refl refl = refl

            ap-γ-refl : ap (unconvert (Rec D cs)) γ-path ≡ refl
            ap-γ-refl =
                ap (ap (unconvert (Rec D cs))) (Σ-≡-intro-refl (ext (pwr-of cs p)))
              • ! (ap-∘ {f = unconvert (Rec D cs)}
                        {g = λ v → (((λ _ → tt) , s) , v)} (ext (pwr-of cs p)))
              • ap-Σ-const (λ v → λ d → v (inl d))
                           (λ v → unconvert cs (s , λ z → v (inr z)))
                           (ext (pwr-of cs p))
              • collapse-Σ-product ap-precomp-inl-refl ap-snd-side-refl

        {-
            Applying an elim then converting the IH agrees with first converting
            (which packages rec slots as a sum) and then applying the elim
            pointwise at each position.
        -}
        convertIH-applyElim :
            (cs : ConstrArity {ℓ}) {C : Type ℓ} {motive : C → Type ℓ}
            (args : Args cs C) (elim : (x : C) → motive x) →
            (z : recPos cs (fst (convert cs args))) →
            convertIH cs args (mkIHs cs elim args) z
            ≡ elim (snd (convert cs args) z)
        convertIH-applyElim Done         _          _    ()
        convertIH-applyElim (Nonrec A k) (a , args) elim z       =
            convertIH-applyElim (k a) args elim z
        convertIH-applyElim (Rec D cs)   (r , args) elim (inl d) = refl
        convertIH-applyElim (Rec D cs)   (r , args) elim (inr z) =
            convertIH-applyElim cs args elim z

        {-
            Lift the per-constructor split to a signature-wide W-type encoding:
            A bundles a constructor label with its shape, and B reads off
            the positions.
        -}
        A : Type ℓ
        A = Σ Op (λ c → Args (arity c) (⊤ {ℓ}))

        B : A → Type ℓ
        B (c , s) = recPos (arity c) s

        wtypeSignature : Signature
        wtypeSignature = WTypeSignature A B

        {-
            Convert per-constructor arguments to W-type arguments. This is
            just a repackaging via `convert`.
        -}
        convertArgs : (c : Op) → (Ty : Type ℓ) → Args (arity c) Ty → Args (Signature.arity wtypeSignature tt) Ty
        convertArgs c Ty args =
            let (s , p) = convert (arity c) args in ((c , s) , p , tt)

        module _ {C : Type ℓ} (indAlg : IndAlg sig C) where
            open IndAlg indAlg

            {-
                The W-type constructor: read off shape and positions, rebuild
                the original args via `unconvert`, then call the original
                constructor.
            -}
            wtypeConstr : ⊤ {ℓ} → Args (Signature.arity wtypeSignature tt) C → C
            wtypeConstr _ ((c , s) , p , tt) = algebra c (unconvert (arity c) (s , p))

            {-
                Translate W-type minor premises back to original minor premises.
            -}
            origMPOfWtypeMP : (motive : C → Type ℓ) →
                Cases wtypeSignature C wtypeConstr motive →
                Cases sig C algebra motive
            origMPOfWtypeMP motive wmp c args ih =
                tpt (λ z → motive (algebra c z)) (unconvert-convert (arity c) args)
                    (wmp tt ((c , fst (convert (arity c) args))
                            , snd (convert (arity c) args)
                            , tt)
                         (convertIH (arity c) args ih , tt))

            wtypeInd : (motive : C → Type ℓ) →
                       Cases wtypeSignature C wtypeConstr motive →
                       (a : C) → motive a
            wtypeInd motive wmp = ind motive (origMPOfWtypeMP motive wmp)

            {-
                Beta for the W-type version. We use the original signature's beta
                and propagate it through the convert/unconvert isomorphism.
            -}
            wtypeBeta : BetaLaw wtypeSignature wtypeInd
            wtypeBeta motive wmp tt ((c , s) , p , tt) =
                let sp' = convert (arity c) (unconvert (arity c) (s , p))
                    target = wmp tt ((c , fst sp') , snd sp' , tt)
                                  ((λ z → wtypeInd motive wmp (snd sp' z)) , tt)
                in
                beta motive (origMPOfWtypeMP motive wmp) c (unconvert (arity c) (s , p))
                -- Step 1: align the IH using `convertIH-applyElim` + funext.
                • ap (tpt (λ z → motive (algebra c z))
                          (unconvert-convert (arity c) (unconvert (arity c) (s , p))))
                     (ap (wmp tt ((c , fst sp') , snd sp' , tt))
                         (Σ-≡-intro (ext (convertIH-applyElim (arity c)
                                                              (unconvert (arity c) (s , p))
                                                              (wtypeInd motive wmp)))
                                    refl))
                -- Step 2: replace `unconvert-convert _ (unconvert _ _)` with
                -- `ap (unconvert _) (convert-unconvert _ _)` via the triangle.
                • ap (λ q → tpt (λ z → motive (algebra c z)) q target)
                     (triangle (arity c) (s , p))
                -- Step 3: J-collapse the transport over `convert-unconvert _ _`.
                • tpt-along-q (convert-unconvert (arity c) (s , p))
              where
                {-
                    Key step. Given any path `q : sp' ≡ sp` between
                    `Σ (Shape (arity c)) (Pos (arity c) → C)`-pairs, J-induction
                    collapses the transport along `ap unconvert q` to identity.
                -}
                tpt-along-q :
                  {sp sp' : Σ (Args (arity c) (⊤ {ℓ}))
                              (λ s → recPos (arity c) s → C)}
                  (q : sp' ≡ sp) →
                  tpt (motive ∘ algebra c) (ap (unconvert (arity c)) q)
                      (wmp tt ((c , fst sp') , snd sp' , tt)
                           ((λ z → wtypeInd motive wmp (snd sp' z)) , tt))
                  ≡ wmp tt ((c , fst sp) , snd sp , tt)
                        ((λ z → wtypeInd motive wmp (snd sp z)) , tt)
                tpt-along-q refl = refl

            indAlgWtype : WTypeIndAlg A B C
            indAlgWtype .IndAlg.algebra = wtypeConstr
            indAlgWtype .IndAlg.ind = wtypeInd
            indAlgWtype .IndAlg.beta = wtypeBeta

            allIndAlgWTypeIndAlg : Σ (Type ℓ) (λ A → Σ (A → Type ℓ)
                (λ B → WTypeIndAlg A B C))
            allIndAlgWTypeIndAlg = (A , B , indAlgWtype)

        {-
            Fidelity of the embedding, fold level: the fold of the
            W-type inductive algebras agrees pointwise with the fold
            of the original ones.
        -}
        module _ {C D : Type ℓ} (iC : IndAlg sig C) (iD : IndAlg sig D) where
            foldW : C → D
            foldW = IndAlg.fold (indAlgWtype iC) (wtypeConstr iD)

            {-
                `foldW` is an algebra homomorphism for the *original*
                constructor algebras: unfold one constructor via the
                W-type β-rule, then push the mapping through
                `unconvert`'s naturality.
            -}
            wtypeFold-hom : (c : Op) (args : Args (arity c) C) →
                foldW (IndAlg.algebra iC c args)
                  ≡ IndAlg.algebra iD c (mapArgs (arity c) foldW args)
            wtypeFold-hom c args =
                  ap (foldW ∘ IndAlg.algebra iC c) (! (unconvert-convert (arity c) args))
                • IndAlg.fold-β (indAlgWtype iC) (wtypeConstr iD) tt
                      ((c , fst sp) , snd sp , tt)
                • ap (IndAlg.algebra iD c) (unconvert-mapArgs (arity c) foldW sp)
                • ap (IndAlg.algebra iD c ∘ mapArgs (arity c) foldW)
                     (unconvert-convert (arity c) args)
              where
                sp = convert (arity c) args

            {-
                Hence `foldW` agrees with the original fold: both are
                algebra homomorphisms out of the same h-initial
                algebra, and folds are unique (`fold-unique`).
            -}
            wtypeFoldAgree : (x : C) →
                foldW x ≡ IndAlg.fold iC (IndAlg.algebra iD) x
            wtypeFoldAgree = fold-unique iC (IndAlg.algebra iD) foldW wtypeFold-hom

        module _ {C D : Type ℓ} (config : Config sig C D) where
            open Config config

            configWTypeConfig : WTypeConfig A B C D
            configWTypeConfig = record
                { indAlgC = indAlgWtype indAlgC
                ; indAlgD = indAlgWtype indAlgD }

            allConfigWTypeConfig : Σ (Type ℓ) (λ A → Σ (A → Type ℓ) (λ B → WTypeConfig A B C D))
            allConfigWTypeConfig = (A , B , configWTypeConfig)

            {-
                Fidelity of the embedding, repair level: the embedding
                does not change the repair equivalence. The forward and
                backward maps of `configToEquiv` for the W-type
                configuration equal those of the original
                configuration — `wtypeFoldAgree` on each side, lifted
                to a map equality by funext.
            -}
            wtypeConfigEquivAgree-f :
                _≃_.f (snd (configToEquiv configWTypeConfig))
                  ≡ _≃_.f (snd (configToEquiv config))
            wtypeConfigEquivAgree-f = ext (wtypeFoldAgree indAlgC indAlgD)

            wtypeConfigEquivAgree-g :
                _≃_.g (snd (configToEquiv configWTypeConfig))
                  ≡ _≃_.g (snd (configToEquiv config))
            wtypeConfigEquivAgree-g = ext (wtypeFoldAgree indAlgD indAlgC)