{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Span
open import lib.types.Paths
import lib.types.Generic1HIT as Generic1HIT
open import lib.types.Pushout

module lib.types.PushoutFlattening {i} {j} {k} {d : Span {i} {j} {k}} where

open Span d renaming (f to g; g to h)

module PushoutRecType {l} (left* : A  Type l) (right* : B  Type l)
  (glue* : (c : C)  left* (g c)  right* (h c)) where

  open PushoutRec left* right* (ua  glue*) public

  abstract
    coe-glue-β : (c : C) (a : left* (g c))
       coe (ap f (glue c)) a == –> (glue* c) a
    coe-glue-β c a =
      coe (ap f (glue c)) a  =⟨ glue-β c |in-ctx  u  coe u a) 
      coe (ua (glue* c)) a   =⟨ coe-β (glue* c) a 
      –> (glue* c) a =∎

    coe!-glue-β : (c : C) (b : right* (h c))
       coe! (ap f (glue c)) b == <– (glue* c) b
    coe!-glue-β c b =
      coe! (ap f (glue c)) b  =⟨ glue-β c |in-ctx  u  coe! u b) 
      coe! (ua (glue* c)) b   =⟨ coe!-β (glue* c) b 
      <– (glue* c) b =∎

    ↓-glue-out : (c : C) {a : left* (g c)} {b : right* (h c)}
       a == b [ f  glue c ]
       –> (glue* c) a == b
    ↓-glue-out c {a} {b} p =
      –> (glue* c) a          =⟨ ! (coe-glue-β c a) 
      coe (ap f (glue c)) a   =⟨ to-transp p 
      b =∎

    ↓-glue-in : (c : C) {a : left* (g c)} {b : right* (h c)}
       –> (glue* c) a == b
       a == b [ f  glue c ]
    ↓-glue-in c {a} {b} p = from-transp f (glue c) (coe-glue-β c a  p)

  private
    module _ where
      fA : Type _
      fA = Σ A left*

      fB : Type _
      fB = Σ B right*

      fC : Type _
      fC = Σ C (left*  g)

      fg : fC  fA
      fg (c , c') = (g c , c')

      fh : fC  fB
      fh (c , c') = (h c , –> (glue* c) c')

    f-d : Span
    f-d = span fA fB fC fg fh

  flattening : Σ (Pushout d) f == Pushout f-d
  flattening = Σ= p p'  q  r  s  where

    module G = PushoutGeneric {d = d}

    P-cc : Coprod A B  Type _
    P-cc (inl a) = left* a
    P-cc (inr b) = right* b

    module P = G.RecType P-cc glue*

    import lib.types.Flattening as Flattening
    module FlatteningPushout = Flattening
      (Coprod A B) C (inl  g) (inr  h) P-cc glue*
    open FlatteningPushout hiding (flattening-equiv; module P)

    p-equiv : Pushout d  G.T
    p-equiv = G.generic-pushout

    p : Pushout d == G.T
    p = ua p-equiv

    p' : f == P.f [  X  (X  Type _))  p ]
    p' = ↓-app→cst-in  {t} {t'} q 
           Pushout-elim {P = λ t  f t == P.f (–> p-equiv t)}
              a  idp)  b  idp)
              c  ↓-='-in'
               (ap (P.f  (–> p-equiv)) (glue c)    =⟨ ap-∘ P.f (–> p-equiv) (glue c) 
                ap P.f (ap (–> p-equiv) (glue c))   =⟨ G.To.glue-β c |in-ctx ap P.f 
                ap P.f (pp c)                       =⟨ P.pp-β c 
                ua (glue* c)                        =⟨ ! (glue-β c) 
                ap f (glue c) =∎))
         t  ap P.f (↓-idf-ua-out _ q))

    --

    module fG' = Generic1HIT At Bt ft gt

    q : Σ G.T P.f == fG'.T
    q = ua FlatteningPushout.flattening-equiv

    --

    {-
    This part is basically [Generic1HIT=] applied to the flattening lemma
    for coproducts. Maybe it would make sense to refactor it that way.
    -}

    module fG = PushoutGeneric {d = f-d}

    r : fG'.T == fG.T
    r = ua (equiv to from to-from from-to)  where

      to-cc : At  fG.T
      to-cc (inl a , a') = fG.cc (inl (a , a'))
      to-cc (inr b , b') = fG.cc (inr (b , b'))

      module To = fG'.Rec to-cc fG.pp

      to : fG'.T  fG.T
      to = To.f

      from-cc : Coprod fA fB  fG'.T
      from-cc (inl (a , a')) = fG'.cc (inl a , a')
      from-cc (inr (b , b')) = fG'.cc (inr b , b')

      module From = fG.Rec from-cc fG'.pp

      from : fG.T  fG'.T
      from = From.f

      abstract
        to-from : (x : fG.T)  to (from x) == x
        to-from = fG.elim to-from-cc to-from-pp  where
          to-from-cc : (x : Coprod fA fB)
             to (from (fG.cc x)) == fG.cc x
          to-from-cc (inl _) = idp
          to-from-cc (inr _) = idp

          to-from-pp : (c : fC)
             idp == idp [  x  to (from x) == x)  fG.pp c ]
          to-from-pp c = ↓-∘=idf-in' to from
            (ap to (ap from (fG.pp c))   =⟨ From.pp-β c |in-ctx ap to 
             ap to (fG'.pp c)            =⟨ To.pp-β c 
             fG.pp c =∎)

        from-to : (x : fG'.T)  from (to x) == x
        from-to = fG'.elim from-to-cc from-to-pp  where
          from-to-cc : (a : At)  from (to (fG'.cc a)) == fG'.cc a
          from-to-cc (inl _ , _) = idp
          from-to-cc (inr _ , _) = idp

          from-to-pp : (b : Bt)
             idp == idp [  x  from (to x) == x)  fG'.pp b ]
          from-to-pp b = ↓-∘=idf-in' from to
            (ap from (ap to (fG'.pp b))   =⟨ To.pp-β b |in-ctx ap from 
             ap from (fG.pp b)            =⟨ From.pp-β b 
             fG'.pp b =∎)

    --

    s : fG.T == Pushout f-d
    s = ! (ua fG.generic-pushout)