{-# OPTIONS --rewriting #-}

open import Agda.Primitive using (Level;lsuc;_⊔_;lzero)
open import Lib
open import Interval
open import Path
open import Equiv
open import Proposition
open import Cofibs
open import Kan
open import Glue

module Glue-Weak where

  Glue-to-fiber : ∀ {l} {α : Set} {{cα : Cofib α}} {T : α → Set l} {B : Set l} {f : (u : α) → T u → B}
                    → (g : Glue α T B f)
                    → ((pα : α) → HFiber (f pα) (unglue g))
  Glue-to-fiber g = (\ pα → (coe (Glue-α _ _ _ _ pα) g ) , (\ _ → unglue g) , ! (unglue-α g pα) , id ) 

  -- repackaging of CCHM final steps
  -- note: this is *almost* rearrangeable into
  --       unglue, glue-to-fiber : Glue α T B f ≃ Σ (x : B). α → HFiber f b
  -- but the equality is strict in the input
  -- and not proved in the output (though it looks like it would be weak)

  glue-weak-better : ∀ {l} {α : Set} {{cα : Cofib α}} {T : α → Set l} {B : Set l} {f : (u : α) → T u → B}
                   → hasHCom B
                   → (β : Set) {{cβ : Cofib β}}
                   → (g : β → (Glue α T B f)) -- already have a partial answer
                   → (b : B [ β ↦ (\ pβ → unglue (g pβ)) ]) 
                   → (t : (pα : α) → HFiber (f pα) (fst b)
                       [ β ↦ (\ pβ → transport (HFiber (f pα))
                                               (snd b pβ)
                                               (Glue-to-fiber (g pβ) pα)) ])
                   → (Glue α T B f) [ β ↦ g ]
  glue-weak-better {α = α} {{ cα }} {T} {f = f} hcomB β g b t =
      g' , (\ pβ → glue-cong _ _ _ _ _ _ (λ= \ pα → ap fst (snd (t pα) pβ) ∘ ! (fst-transport-HFiber-base (f pα) (snd b pβ) (Glue-to-fiber (g pβ) pα)))
                                         (fst (snd fix) (inr pβ)) ∘ Glueη (g pβ)) where
       fix = hcomB `1 `0
                      (α ∨ β)
                      (\ x → case (\ pα →  fst (snd (fst (t pα))) x )
                                  (\ pβ → unglue (g pβ))
                                  (\ pα pβ →  ap= (fst-snd-transport-HFiber-base (f pα) (snd b pβ) (Glue-to-fiber (g pβ) pα))
                                              ∘ ! (ap (\ H → fst (snd H) x) (snd (t pα) pβ)))) 
                      (fst b ,  ∨-elim _
                                       (\ pα → snd (snd (snd (fst (t pα)))) )
                                       (\ pβ → snd b pβ)
                                       (\ _ _ → uip)  )

       g' = glue _ _ _ _ (\ pα →  fst (fst (t pα)) )
                         (fst fix ,
                          (\ pα → fst (snd fix) (inl pα) ∘ ! (fst (snd (snd (fst (t pα)))))))

  -- this version makes the η definitional if you specify up front that you want it
  glue-weak-better-η : ∀ {l} {α : Set} {{cα : Cofib α}} {T : α → Set l} {B : Set l} {f : (u : α) → T u → B}
                     → (hb : hasHCom B)
                     → (g : Glue α T B f)
                     → fst (glue-weak-better {α = α} {{cα}}{T}{B}{f} hb (`0 == `0) (\ _ → g) (unglue g , (\ _ → id)) (\ pα → (Glue-to-fiber g pα , (\ _ → id))))
                       == g
  glue-weak-better-η hb g = ! (snd (glue-weak-better hb (`0 == `0) (\ _ → g) (unglue g , (\ _ → id)) (\ pα → (Glue-to-fiber g pα , (\ _ → id)))) id)