```{-# 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

cβ : Contractβ
cβ _ = 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 → cβ (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
```