{-# OPTIONS --rewriting #-}

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

module universe.Sigma where
  
  ΣData : (@♭ l1 l2 : Level) → Set _
  ΣData l1 l2 = Σ \ (A : U{l1}) → (El A → U {l2})

  Σ-from-data : ∀ {@♭ l1 l2 : Level} → ΣData l1 l2 → Set _
  Σ-from-data (A , B) = Σ \ (x : El A) → El (B x)

  comΣ : ∀ {@♭ l1 l2 : Level} → relCom {Γ = (ΣData l1 l2)} Σ-from-data
  comΣ AB r r' α t b = ((fst (filla b r')) , fst (comb b)) , 
                        (\ pα → pair= (fst (snd (filla b r')) pα) (fst (snd (comb b)) pα)) ,
                        ((\ {id → pair= (snd (snd (filla b r')) id) (snd (snd (comb b)) id)})) where
    A = \ x → fst (AB x)
    B = \ xa → snd (AB (fst xa)) (snd xa)

    filla : (b : _) (z : I) → _
    filla b z = (comEl A r z α (\ pα z → fst (t pα z)) (fst (fst b) , (\ pα → ap fst (snd b pα))))

    comb : (b : _) → _
    comb b = 
      (comEl (\ z → B (z , (fst (filla b z))))
              r r' 
              α (\ z pα →  transport (El o (B o \ h → (z , h))) (fst (snd (filla b z)) pα) (snd (t z pα)) )
                (transport (El o B o \ h → (r , h)) (snd (snd (filla b r)) id) (snd (fst b)) , 
                (\ pα → ap (transport (El o B o (λ h → r , h)) (snd (snd (filla b r)) id)) (apd snd (snd b pα) ∘ ! (ap= (transport-ap-assoc' (λ z → El (B (r , z))) fst (snd b pα))) ) ∘ ap= (transport-∘ (El o B o (λ h → r , h)) (snd (snd (filla b r)) id) (ap fst (snd b pα))) ∘ ap {M = (fst (snd (filla b r)) pα)} {N = (snd (snd (filla b r)) id ∘ ap fst (snd b pα))} (\ h → transport (El o B o (λ h → r , h)) h (snd (t r pα))) uip)))

  Σcode-universal : ∀ {@♭ l1 l2 : Level} 
                  → (Σ \ (A : U {l1}) → El(A) → U{l2}) → U{l1 ⊔ l2}
  Σcode-universal {l1} {l2} = code (ΣData l1 l2) 
                             (\ AB → Σ \ (x : El (fst AB)) → El (snd AB x))
                             comΣ

  Σcode : ∀ {@♭ l1 l2 l3 : Level} {Γ : Set l1} (A : Γ → U{l2}) (B : Σ (El o A) → U{l3}) → (Γ → U{l2 ⊔ l3})
  Σcode {l1} {l2} {l3} A B = Σcode-universal {l2} {l3} o (\ x → (A x , \ y → B (x , y)))

  Σcode-stable : ∀ {@♭ l1 l2 l3 l4 : Level} {Γ : Set l1} {Δ : Set l3} (A : Γ → U{l2}) (B : Σ (El o A) → U{l4})
                   {θ : Δ → Γ}
               → ((Σcode A B) o θ) == Σcode (A o θ) (B o (\ p → (θ (fst p) , snd p)))
  Σcode-stable A B = id

  El-Σcode : ∀ {@♭ l1 l2 l3 : Level} {Γ : Set l1} (A : Γ → U{l2}) (B : Σ (El o A) → U{l3})
           → (g : Γ) → El (Σcode A B g) == (Σ \ (x : El (A g)) → El (B (g , x)))
  El-Σcode A B g = id