{-# OPTIONS --rewriting #-}

open import Agda.Primitive using (Level;lsuc;_⊔_;lzero)
open import Lib
open import Interval
open import Proposition
open import Cofibs
open import Kan
open import Equiv
open import universe.Universe
open import Glue
open import Path
open import universe.Pi
open import universe.Sigma
open import universe.Glue
open import universe.Path
open import universe.U
open import Contractible

module universe.Univalence where

  
  ua : {@♭ l : Level} {A B : U{l}} (e : Equiv (El A) (El B)) → Path U A B
  ua {l}{A}{B} e = (\ x → Glue-code-universal (V-to-Glue (Vc A B e x)))  , 
                          Glue-code-universal-α (V-to-Glue (Vc A B e `0)) (inl id) , 
                          Glue-code-universal-α (V-to-Glue (Vc A B e `1)) (inr id)

  uaβ : {@♭ l : Level} {A B : U{l}} (e : Equiv (El A) (El B)) (a : El A)
        → Path _ (coePathU (ua{_}{A}{B} e) a) (fst e a)
  uaβ {l}{A}{B} e a =  (\ z → coe (ap El (snd (snd UA))) (fst combined z)) ,
                       ! (ap (coe (ap El (snd (snd UA)))) reduce) ∘ ap (coe (ap El (snd (snd UA)))) (fst (snd combined)) ,
                       (ap {M = (ap El (snd (snd UA)) ∘ ap El (! (snd (snd UA))))} {N = id} (\ H → coe H (fst e a)) uip ∘ ! (ap= (transport-∘ (\ X → X) (ap El (snd (snd UA))) (ap El (! (snd (snd UA)))))) ) ∘ ap (coe (ap El (snd (snd UA)))) (snd (snd combined))   where
    UA = (ua{_}{A}{B} e)
    a' = (coe (ap El (! (fst (snd UA)))) a)

    reduce : fst (coeU (fst UA) `0 `1 a') == fst (comGlue (\ x → (V-to-Glue (Vc A B e x))) `0 `1 ⊥ (\ x → abort) (a' , \ x → abort x))
    reduce = fst (coeU (fst UA) `0 `1 a') =〈 id 〉
              fst (relCom-relCoe (El o (fst UA)) (comEl' (fst UA)) (\ x → x) `0 `1 a') =〈 ap (\ H → fst (relCom-relCoe (El o (fst UA)) H (\ x → x) `0 `1 a')) reduce2 〉
              fst (relCom-relCoe (El o (fst UA)) (comPre (\ x → (V-to-Glue (Vc A B e x))) (Glue-from-data) comGlue) (\ x → x) `0 `1 a') =〈 id 〉
              fst (comPre (\ x → (V-to-Glue (Vc A B e x))) (Glue-from-data) comGlue (\ x → x) `0 `1 ⊥ (\ x → abort) (a' , \ x → abort x)) =〈 id 〉
              (fst (comGlue (\ x → (V-to-Glue (Vc A B e x))) `0 `1 ⊥ (\ x → abort) (a' , \ x → abort x)) ∎) where
        reduce2 : (comEl' (fst UA)) == comPre (\ x → (V-to-Glue (Vc A B e x))) (Glue-from-data) comGlue 
        reduce2 = comEl-code-subst {A = Glue-from-data} {comA = comGlue} (\ x → (V-to-Glue (Vc A B e x)))

    -- would be an equality with propositional univalence for cofibs
    eq : Path _ (fst (comGlue (\ x → (V-to-Glue (Vc A B e x))) `0 `1 ⊥ (\ x → abort) (a' , \ x → abort x)))
                (fst (comGlue-unaligned (\ x → (V-to-Glue (Vc A B e x))) `0 `1 ⊥ (\ x → abort) (a' , \ x → abort x)))
    eq = comGlue-not∀α (\ x → (V-to-Glue (Vc A B e x))) (not0∨1) `0 `1 ⊥ (\ x → abort) (a' , \ x → abort x)

    unaligned : Path _
                (fst (comGlue-unaligned (\ x → (V-to-Glue (Vc A B e x))) `0 `1 ⊥ (\ x → abort) (a' , \ x → abort x)))
                (coe (ap El (! (snd (snd UA)))) (fst e a))
    unaligned = (\ z → coe (ap El (! (snd (snd UA)))) (fst (comGlue-unaligned-β-V-coe {A = A}{B} e a) z)) ,
                ( ( ap {M = (! (Glue-α ((`0 == `0) ∨ (`0 == `1)) (El o GlueData.T (V-to-Glue (Vc A B ((λ z → fst e z) , snd e) `0))) (El (GlueData.B (V-to-Glue (Vc A B ((λ z → fst e z) , snd e) `0)))) (GlueData.f (V-to-Glue (Vc A B ((λ z → fst e z) , snd e) `0))) (inl id)))} {N = (ap El (! (fst (snd UA))))} (\ H → (fst (comGlue-unaligned (λ x → V-to-Glue (Vc A B ((λ z → fst e z) , snd e) x)) `0 `1 ⊥ (λ x → abort) (coe H a , (λ x → abort x))))) uip ∘ ap {M = (ap El (! (snd (snd UA))) ∘ Glue-α ((`1 == `0) ∨ (`1 == `1)) (El o GlueData.T (V-to-Glue (Vc A B e `1))) (El (GlueData.B (V-to-Glue (Vc A B e `1)))) (GlueData.f (V-to-Glue (Vc A B e `1))) (inr id))} {N = id} (\ H → coe H (fst (comGlue-unaligned (λ x → V-to-Glue (Vc A B ((λ z → fst e z) , snd e) x)) `0 `1 ⊥ (λ x → abort) (coe (! (Glue-α ((`0 == `0) ∨ (`0 == `1)) (El o GlueData.T (V-to-Glue (Vc A B ((λ z → fst e z) , snd e) `0))) (El (GlueData.B (V-to-Glue (Vc A B ((λ z → fst e z) , snd e) `0)))) (GlueData.f (V-to-Glue (Vc A B ((λ z → fst e z) , snd e) `0))) (inl id))) a , (λ x → abort x))))) uip ) ∘ ! (ap= (transport-∘ (\ X → X) (ap El (! (snd (snd UA)))) (Glue-α ((`1 == `0) ∨ (`1 == `1)) (El o GlueData.T (V-to-Glue (Vc A B e `1))) (El (GlueData.B (V-to-Glue (Vc A B e `1)))) (GlueData.f (V-to-Glue (Vc A B e `1))) (inr id)))) ) ∘ ap (coe (ap El (! (snd (snd UA))))) (fst (snd (comGlue-unaligned-β-V-coe e a)))  ,
                ap (coe (ap El (! (snd (snd UA))))) (snd (snd (comGlue-unaligned-β-V-coe e a)))

    combined = ∘Path (hcomEl (Glue-code (\ (_ : Unit{lzero}) → (V-to-Glue (Vc A B e `1))) <>) ) unaligned eq