# Pastebin J8mjFOIk
{-# OPTIONS --cubical --rewriting #-}

open import Cubical.FromStdLib
open import Cubical.PathPrelude as P hiding ( _≃_ ; idEquiv )
open import Cubical.GradLemma
open import Cubical.PushOut renaming ( P to Pushout ; primPushOutElim to Pushout-elim )
open import Cubical.Univalence

module Cubical.Examples.Flattening {l k}
  {A B C : Set l} (f : C → A) (g : C → B)
  (Dₗ : A → Set k)
  (Dᵣ : B → Set k)
  (Dₚ : (c : C) → Dₗ (f c) ≃ Dᵣ (g c))
  where

private
  module _ {ℓ} {A B : Set ℓ} (f : A ≃ B) where
    –> : A → B
    –> = _≃_.eqv f

    <– : B → A
    <– = (fst ∘ fst) ∘ (_≃_.isEqv f)

    <–-inv-r : ∀ b → –> (<– b) ≡ b
    <–-inv-r b = sym (snd (fst (_≃_.isEqv f b)))

    <–-inv-l : ∀ a → <– (–> a) ≡ a
    <–-inv-l a = cong fst (snd (_≃_.isEqv f (–> a)) (a , refl))

D : Pushout f g → Set k
D = Pushout-elim _ Dₗ Dᵣ (ua ∘ Dₚ)

totf : Σ C (Dₗ ∘ f) → Σ A Dₗ
totf (c , d) = (f c , d)

totg : Σ C (Dₗ ∘ f) → Σ B Dᵣ
totg (c , d) = (g c , –> (Dₚ c) d)

explain : (c : C) → Path {A = Path (Dₗ (f c)) (Dᵣ (g c))} (λ i → D (push c i)) (λ i → ua (Dₚ c) i)
explain c = refl

ua-glue : ∀ {ℓ} {A B : Set ℓ} (f : A ≃ B) → PathP (λ i → A → ua f i) (idFun A) (–> f)
ua-glue f i a = glue {φ = ~ i ∨ i} (λ { (i = i0) → a ; (i = i1) → –> f a }) (–> f a)

ua-unglue : ∀ {ℓ} {A B : Set ℓ} (f : A ≃ B) → PathP (λ i → ua f i → B) (–> f) (idFun B)
ua-unglue f i y = unglue {φ = ~ i ∨ i} y

toTot : Σ (Pushout f g) D → Pushout totf totg
toTot = uncurry goal
  where
  have : (c : C) → PathP (λ i → D (push c i) → Pushout totf totg)
                         (λ y → inl (f c , <– (Dₚ c) (–> (Dₚ c) y)))
                         (λ y → inr (g c , –> (Dₚ c) (<– (Dₚ c) y)))
  have c i y = push (c , (<– (Dₚ c) (ua-unglue (Dₚ c) i y))) i

  hole : (c : C) → PathP (λ i → D (push c i) → Pushout totf totg)
                         (λ y → inl (f c , y)) (λ y → inr (g c , y))
  hole c = transp
    (λ k → PathP (λ i → D (push c i) → Pushout totf totg) (λ y → inl (f c , <–-inv-l (Dₚ c) y k)) (λ y → inr (g c , <–-inv-r (Dₚ c) y k)))
    (have c)

  goal : (x : Pushout f g) (y : D x) → Pushout totf totg
  goal = Pushout-elim _ (curry inl) (curry inr) hole

fromTot : Pushout totf totg → Σ (Pushout f g) D
fromTot = Pushout-elim _
  (λ { (a , d) → (inl a , d) })
  (λ { (b , d) → (inr b , d) })
  (λ { (c , d) → λ i → (push c i , ua-glue (Dₚ c) i d) })


toFromTot : (x : Pushout totf totg) → toTot (fromTot x) ≡ x
toFromTot = Pushout-elim _
  (λ _ → refl)
  (λ _ → refl)
  (λ { (c , d) → idFun (PathP (λ i → toTot (fromTot (push (c , d) i)) ≡ push (c , d) i) refl refl) {!!} })