{-# OPTIONS --without-K #-}
open import Agda.Primitive
open import 1-equality
open import 2-composition
open import 2-ski
open import 3-ap
open import 4-homotopy
open import 4-transport
open import 5-qip
open import 6-equivalence
open import 7-dependentpairs

elim[Π≡Π] :
  {ℓ₁ ℓ₂ : Level}        
  {A : Set ℓ₁}           
  {B : A  Set ℓ₂}       
  {f g : Π A B}          
  f  g                  
  f  g

elim[Π≡Π] refl = refl[∼]

postulate
  intr[Π≡Π] :
    {ℓ₁ ℓ₂ : Level}       
    {A : Set ℓ₁}          
    {B : A  Set ℓ₂}      
    {f g : Π A B}         
    f  g                 
    f  g

postulate
  weakuniq[Π≡Π] :
    {ℓ₁ ℓ₂ : Level}                   
    {A : Set ℓ₁}                      
    {B : A  Set ℓ₂}                  
    {f : Π A B}                       
    (intr[Π≡Π]  elim[Π≡Π])  id' (f  f)

uniq[Π] :
  {ℓ₁ ℓ₂ : Level}                   
  {A : Set ℓ₁}                      
  {B : A  Set ℓ₂}                  
  {f g : Π A B}                     
  intr[Π≡Π]  elim[Π≡Π]  id' (f  g)

uniq[Π] {f = f} {g = f} refl = weakuniq[Π≡Π] refl

postulate
  elim[Π≡Π]·is·epic :
    {ℓ₁ ℓ₂ ℓ₃ : Level}                
    {A : Set ℓ₁}                      
    {B : A  Set ℓ₂}                  
    {f g : Π A B}                     
    {C : Set ℓ₃}                      
    {F G : (f  g)  C}               
    (F  elim[Π≡Π]  G  elim[Π≡Π])   
    F  G

comp[Π] :
  {ℓ₁ ℓ₂ : Level}                   
  {A : Set ℓ₁}                      
  {B : A  Set ℓ₂}                  
  {f g : Π A B}                     
  elim[Π≡Π]  intr[Π≡Π]  id' (f  g)

comp[Π] = elim[Π≡Π] (elim[Π≡Π]·is·epic (intr[Π≡Π] (elim[Π≡Π]
  (ass[∘] elim[Π≡Π] intr[Π≡Π] elim[Π≡Π]) •[∼] (elim[Π≡Π] ∘∼ uniq[Π]))))

∼≃≡ :
  {ℓ₁ ℓ₂ : Level}   
  {A : Set ℓ₁}      
  {B : A  Set ℓ₂}  
  {f g : Π A B}     
  (f  g)  (f  g)

∼≃≡ =
  QIP·to·≃
  QIP[ intr[Π≡Π]
     , elim[Π≡Π]
     , uniq[Π]
     , comp[Π] ]

comp·refl[Π] :
  {ℓ₁ ℓ₂ : Level}              
  {A : Set ℓ₁}                 
  {B : A  Set ℓ₂}             
  {f : Π A B}                  
  intr[Π≡Π] refl[∼]  refl' f

comp·refl[Π] = uniq[Π] refl

comp·sym[Π] :
  {ℓ₁ ℓ₂ : Level}              
  {A : Set ℓ₁}                 
  {B : A  Set ℓ₂}             
  {f g : Π A B}                
  (α : f  g)                  
  intr[Π≡Π] (sym[∼] (elim[Π≡Π] α))  sym α

comp·sym[Π] refl = uniq[Π] refl

comp·•[Π] :
  {ℓ₁ ℓ₂ : Level}              
  {A : Set ℓ₁}                 
  {B : A  Set ℓ₂}             
  {f g h : Π A B}              
  (α : f  g)                  
  (β : g  h)                  
  intr[Π≡Π] (elim[Π≡Π] α •[∼] elim[Π≡Π] β)  α  β

comp·•[Π] refl refl = uniq[Π] refl

comp·transport[→] :
  {ℓ₁ ℓ₂ ℓ₃ : Level}                 
  {X : Set ℓ₁}                       
  {A : X  Set ℓ₂}                   
  {B : X  Set ℓ₃}                   
  {x₁ x₂ : X}                        
  (p : x₁  x₂)                      
  (f : A x₁  B x₁)                  
  let
    A→B = λ x  (A x  B x)
    g = λ a  f (transport A (sym p) a)
  in
  transport A→B p f  λ a  transport B p (g a)

comp·transport[→] refl _ = intr[Π≡Π] refl[∼]

comp·transport[Π] :
  {ℓ₁ ℓ₂ ℓ₃ : Level}                  
  {X : Set ℓ₁}                        
  {A : X  Set ℓ₂}                    
  {B : (x : X)  A x  Set ℓ₃}      
  {x₁ x₂ : X}                         
  (p : x₁  x₂)                       
  (f : Π (A x₁) λ a  B x₁ a)         
  (a : A x₂)                          
  let
    P = λ x  Π (A x) (B x)
    Q = λ {[ w₁ , w₂ ]  B w₁ w₂}
    q = sym (intr[Σ≡Σ] [ sym p , refl ])
    g = λ a  f (transport A (sym p) a)
  in
  transport P p f a  transport Q q (g a)

comp·transport[Π] refl f a = refl

Lemma·2·9·6 :
  {ℓ₁ ℓ₂ ℓ₃ : Level}                  
  {X : Set ℓ₁}                        
  {A : X  Set ℓ₂}                    
  {B : X  Set ℓ₃}                    
  {x₁ x₂ : X}                         
  (p : x₁  x₂)                       
  (f : A x₁  B x₁)                   
  (g : A x₂  B x₂)                   
  let
    Aᵀ : A x₁  A x₂
    Aᵀ = transport A p
    Bᵀ : B x₁  B x₂
    Bᵀ = transport B p
    A→B = λ x  (A x  B x)
    A→Bᵀ : A→B x₁  A→B x₂
    A→Bᵀ = transport A→B p
  in
  (A→Bᵀ f  g)  (Bᵀ  f  g  Aᵀ)

Lemma·2·9·6 {A = A} {B = B} {x₁ = x₁} {x₂ = x₂} refl f g =
  ≃[ id , id , id , refl[∼] , refl[∼] ]

Lemma·2·9·7 :
  {ℓ₁ ℓ₂ ℓ₃ : Level}                
  {X : Set ℓ₁}                      
  {A : X  Set ℓ₂}                  
  {B : (Σ X A)  Set ℓ₃}            
  {x₁ x₂ : X}                       
  (p : x₁  x₂)                     
  (f : (a : A x₁)  B [ x₁ , a ] )  
  (g : (a : A x₂)  B [ x₂ , a ] )  
  let
    Aᵀ : A x₁  A x₂
    Aᵀ = transport A p
    Bᵀ : (a : A x₁)  B [ x₁ , a ]  B [ x₂ , Aᵀ a ]
    Bᵀ = λ a  transport B (path·lift A p a)
    ΠAB : (x : X)  Set (ℓ₂  ℓ₃)
    ΠAB = λ x  (a : A x)  B [ x , a ]
    ΠABᵀ : ΠAB x₁  ΠAB x₂
    ΠABᵀ = transport ΠAB p
  in
  (ΠABᵀ f  g)  (Bᵀ ∘' f  g  Aᵀ)

Lemma·2·9·7 refl f g =
  QIP·to·≃
  QIP[ elim[Π≡Π] , intr[Π≡Π] , comp[Π] , uniq[Π] ]

sym∘sym≡id :
  { : Level}   
  {A : Set }   
  {x y : A}     
  sym  sym  id' (x  y)

sym∘sym≡id = intr[Π≡Π] λ { refl   refl }

ΠΠ≃Σ→ :
  {ℓ₁ ℓ₂ ℓ₃ : Level}               
  (X : Set ℓ₁)                     
  (Y : X  Set ℓ₂)                 
  ((x : X)  Y x  Set ℓ₃)  ((Σ X Y)  Set ℓ₃)

ΠΠ≃Σ→ X Y = QIP·to·≃
  QIP[  f  λ { [ x , y ]  f x y})
     ,  f  λ { x y  f [ x , y ]})
     , refl[∼]
     , refl[∼] ]