{-# OPTIONS --without-K #-}

open import PropEqWithoutK
open import Agda.Primitive using (Level; _⊔_)

----------------------------------------------------------------------
-- Dependent products
----------------------------------------------------------------------
infixr 4 _,_
record Σ {a b} (A : Set a) (B : A  Set b) : Set (a  b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

-- The syntax declaration below is attached to Σ-syntax, to make it
-- easy to import Σ without the special syntax.

infix 2 Σ-syntax

Σ-syntax :  {a b} (A : Set a)  (A  Set b)  Set (a  b)
Σ-syntax = Σ

syntax Σ-syntax A  x  B) = Σ[ x ∈ A ] B

-- Extensionality for sums
Σext :
  {A : Set}
  {B : A  Set}
  {a a' : A}
  {b : B a}
  {b' : B a'}
  (p : a  a')
  (q : subst B p b  b')
   ---------------------
  (a , b)  (a' , b')
Σext refl refl = refl

----------------------------------------------------------------------
-- The Unit type
----------------------------------------------------------------------
record  : Set where
  instance constructor tt

----------------------------------------------------------------------
-- Standard definitions
----------------------------------------------------------------------
-- Contractibility
isContr : {l : Level}  Set l  Set l
isContr A = Σ[ a₀  A ] ((x : A)  a₀  x)

-- Singletons
Sing : {A : Set}  A  Set
Sing {A} a₀ = Σ[ a  A ] a₀  a

-- Singletons are contractible
singContr : {A : Set}(a₀ : A)  isContr (Sing a₀)
proj₁ (singContr a₀) = (a₀ , refl)
proj₂ (singContr a₀) (.a₀ , refl) = refl

-- The fibers of a function
fib : {l l' : Level}{A : Set l}{B : Set l'}(f : A  B)(b : B)  Set (l'  l)
fib {A = A} f b = Σ[ a  A ] f a  b

-- Equivalences in terms of contractible fibers
isEquiv : {l l' : Level}{A : Set l}{B : Set l'}(f : A  B)  Set (l'  l)
isEquiv {A = A} {B} f = (b : B)  isContr (fib f b)

Equiv : Set  Set  Set
Equiv A B = Σ[ f  (A  B) ] isEquiv f

-- Coercion is defined from transport/substitution
coerce : {A B : Set}  A  B  A  B
coerce = subst  X  X)

----------------------------------------------------------------------
-- Axioms for producing paths
----------------------------------------------------------------------
-- The three axioms
UnitRight = (A : Set)  A  (Σ[ _  A ] )
Flip = {A B : Set}{C : A  B  Set}  (Σ[ a  A ] Σ[ b  B ] C a b)  (Σ[ b  B ] Σ[ a  A ] C a b)
Contract = {A : Set}  isContr A  A  

-- One part of univalence
UA = {A B : Set}  Equiv A B  A  B

-- All three axioms follow from UA
A≅ΣA⊤ : {A : Set}  Equiv A (Σ[ _  A ] )
A≅ΣA⊤ {A} = (f , e) where
  f : A  Σ[ _  A ] 
  f a = (a , tt)
  e : isEquiv f
  e (a , tt) = (a , refl) , (λ{ (.a , refl)  refl })
ua-implies-ur : UA  UnitRight
ua-implies-ur ua A = ua A≅ΣA⊤

ΣABC≅ΣBAC : {A B : Set}{C : A  B  Set}
   Equiv (Σ[ a  A ] Σ[ b  B ] C a b) (Σ[ b  B ] Σ[ a  A ] C a b)
ΣABC≅ΣBAC {A} {B} {C} = (f , e) where
  f : Σ[ a  A ] Σ[ b  B ] C a b  Σ[ b  B ] Σ[ a  A ] C a b
  f (a , b , c) = (b , a , c)
  e : isEquiv f
  e (b , a , c) = ((a , b , c) , refl) , (λ{ (_ , refl)  refl })
ua-implies-flip : UA  Flip
ua-implies-flip ua {A} {B} {C} = ua ΣABC≅ΣBAC

ua-implies-contract : UA  Contract
ua-implies-contract ua {A} (a , all-eq) = ua (f , e) where
  f : A  
  f a = tt
  ⊤-isSet : {x : }{p : x  x}  p  refl
  ⊤-isSet {p = refl} = refl
  e : isEquiv f
  e tt = (a , refl) , (λ{ (a' , refl)  Σext (all-eq a') (⊤-isSet)})

postulate
  unit-r   : UnitRight
  flip     : Flip
  contract : Contract

----------------------------------------------------------------------
-- Function extensionality
----------------------------------------------------------------------
happly : {l l' : Level}{A : Set l}{B : Set l'}{f g : A  B}  f  g  ((x : A)  f x  g x)
happly refl _ = refl

postulate
  funext-full : {l l' : Level}{A : Set l}{B : Set l'}{f g : A  B}  isEquiv (happly {l} {l'} {A} {B} {f} {g})

funext : {l l' : Level}{A : Set l}{B : Set l'}{f g : A  B}  ((x : A)  f x  g x)  f  g
funext ptwise = proj₁ (proj₁ (funext-full ptwise))

-- Derive fibext from funext
fibext : {A : Set}{B B' : A  Set}  ((x : A)  B x  B' x)  Σ A B  Σ A B'
fibext {A} p = cong  B  Σ A B) (funext p)

----------------------------------------------------------------------
-- UA follows from the axioms
----------------------------------------------------------------------
open ≡-Reasoning

ua : UA
ua {A} {B} (f , e) =
    A
  ≡⟨ unit-r A 
    Σ A  _  )
  ≡⟨ fibext  a  sym (contract (singContr (f a)))) 
    (Σ[ a  A ] Σ[ b  B ] f a  b)
  ≡⟨ flip 
    (Σ[ b  B ] Σ[ a  A ] f a  b)
  ≡⟨ fibext  b  contract (e b)) 
    Σ B  _  )
  ≡⟨ sym (unit-r B) 
    B
  

----------------------------------------------------------------------
-- Axioms for transporting along paths
----------------------------------------------------------------------

-- The assumptions we make
UnitRightβ = (A : Set)  coerce (unit-r A)  λ a  (a , tt)
Flipβ = {A B : Set}{C : A  B  Set}  coerce (flip {A} {B} {C})  (λ{(a , b , c)  (b , a , c)})

-- The other half of univalence
UAβ : UA  Set₁
UAβ ua = {A B : Set}(e : Equiv A B)  coerce (ua e)  proj₁ e

-- These properties follow from UAβ
uaβ-implies-urβ : (ua : UA)  UAβ ua  (A : Set)  coerce (ua-implies-ur ua A)  λ a  (a , tt)
uaβ-implies-urβ ua uaβ A = uaβ A≅ΣA⊤

uaβ-implies-fβ : (ua : UA)  UAβ ua  {A B : Set}{C : A  B  Set}
   coerce (ua-implies-flip ua {A} {B} {C})  (λ{ (a , b , c)  (b , a , c)})
uaβ-implies-fβ ua uaβ = uaβ ΣABC≅ΣBAC

postulate
  urβ : UnitRightβ
  flipβ : Flipβ

-- We also want to know the following
UnitRightSymβ = (A : Set)  coerce (sym (unit-r A))  proj₁
Contractβ = {A : Set}(c : isContr A)  coerce (contract c)   _  tt)
ContractSymβ = {A : Set}(c : isContr A)  coerce (sym (contract c))   _  proj₁ c)
FunExtβ = {A : Set}{B B' : A  Set}(p : (x : A)  B x  B' x)
  (a : A)  subst  B  B a) (funext p)  coerce (p a) 

-- We can prove these properties
ursβ : UnitRightSymβ
ursβ A = coe-sym (unit-r A) proj₁ (cong  f   x  proj₁ (f x))) (urβ A)) where
  coe-sym : {A B : Set}(p : A  B)(g : B  A)(inv :  x  g (coerce p x))   x  x))  coerce (sym p)  g
  coe-sym refl g inv = sym inv
  
 : Contractβ
 _ = funext  x  refl)

csβ : ContractSymβ
csβ (a , all-eq) = funext  u  sym (all-eq (coerce (sym (contract (a , all-eq))) u)))

feβ : FunExtβ
feβ {A = A} ptwise a = trans (helper (funext ptwise)) (cong  p  coerce (p a)) happly∘funext=id) where
  helper : {B B' : A  Set}(p : B  B')  subst  B  B a) p  coerce (happly p a)
  helper refl = refl
  happly∘funext=id : happly (funext ptwise)  ptwise
  happly∘funext=id = proj₂ (proj₁ (funext-full ptwise))

-- Deriving a similar property for fibext
feβ' : {A : Set}{B B' : A  Set}(p : (x : A)  B x  B' x)
  {f : (a : A)  B a  B' a}
   ((a : A)  coerce (p a)  f a)
   coerce (fibext {A} {B} {B'} p)  (λ{ (a , b)  (a , f a b)})
feβ' p {f} subst-eq =
  begin
    coerce (fibext p)
  ≡⟨ subst-cong (funext p) 
    (λ{ (a , b)  (a , subst  B  B a) (funext p) b)})
  ≡⟨ funext (λ{ (a , b)  Σext refl (cong-app (trans (feβ p a) (subst-eq a)) b)}) 
    (λ{ (a , b)  (a , f a b)})
  
    where
      subst-cong : {A : Set}{B B' : A  Set}(p : B  B')
         coerce (cong (Σ A) p)  (λ{ (a , b)  (a , subst  B  B a) p b)})
      subst-cong refl = refl


----------------------------------------------------------------------
-- Proof that UAβ follows from these properties
----------------------------------------------------------------------

uaβ : UAβ ua
uaβ {A} {B} e = split-subst
    {p = unit-r A}{fibext  a  sym (contract (singContr (proj₁ e a))))}
    {flip}{fibext  b  contract (proj₂ e b))}{sym (unit-r B)}
    (urβ A) (feβ'  a  sym (contract (singContr (proj₁ e a))))  a  csβ (singContr (proj₁ e a))))
    flipβ (feβ'  b  contract (proj₂ e b))  b   (proj₂ e b))) (ursβ B) refl
      where
        split-subst :
          {A B C D E F G : Set}
          {p : A  B}{q : B  C}{r : C  D}{s : D  E}{t : E  F}{u : F  G}
          {f : A  B}{g : B  C}{h : C  D}{i : D  E}{j : E  F}{k : F  G}
          (p-eq : coerce p  f)(q-eq : coerce q  g)
          (r-eq : coerce r  h)(s-eq : coerce s  i)
          (t-eq : coerce t  j)(u-eq : coerce u  k)
          
          coerce (trans p (trans q (trans r (trans s (trans t u)))))   x  k (j (i (h (g (f x))))))
        split-subst {p = refl} {refl} {refl} {refl} {refl} {refl} refl refl refl refl refl refl = refl