javra/HoTT.agda

## HoTT.agda
{-# OPTIONS --type-in-type --without-K #-}

module HoTT where

U = Set4

data Zero : U where

data One : U where
  star : One

data Two : U where
  starone : Two
  startwo : Two

Not : U → U
Not A = (A → Zero)

notnot : (A : U) → A → Not (Not A)
notnot A a f = f a

notnotnot : (A : U) → Not (Not (Not A)) → Not A
notnotnot A f a = f (notnot A a)

data _+_ : U → U → U where
  inl : {A B : U} → A → A + B
  inr : {A B : U} → B → A + B

rec+ : (A B C : U) → (A → C) → (B → C) → (A + B) → C
rec+ A B C f g (inl a) = f a
rec+ A B C f g (inr b) = g b

restrl : {A B C : U} → ((A + B) → C) → A → C
restrl f a = f (inl a)

restrr : {A B C : U} → ((A + B) → C) → B → C
restrr f b = f (inr b)

notnotlem : (A : U) → Not (Not ((Not A) + A))
notnotlem A f = f (inl (restrr f))

id : {A : U} → A → A
id x = x

swap : {A B C : U} → (A → B → C) → B → A → C
swap f b a = f a b

data _≈_ : {A : U} → A → A → U where
  refl : {A : U} → (x : A) → (x ≈ x)

ind≈ : {A : U} (C : (x y : A) → (x ≈ y) → U) → ((x : A) → C x x (refl x)) → {x y : A} (p : x ≈ y) → C x y p
ind≈ C c (refl x) = c x

ind≈' : {A : U} {a : A} (C : ((x : A) → a ≈ x → U)) → C a (refl a) → {x : A} (p : a ≈ x) → C x p
ind≈' {A}{a} C c {.a} (refl .a) = c

ind≈'' : {A : U} {a : A} (C : ((x : A) → x ≈ a → U)) → C a (refl a) → {x : A} (p : x ≈ a) → C x p
ind≈'' {A}{a} C c {.a} (refl .a) = c

disc≈ : {A : U} → (P : A → U) → {x y : A} → x ≈ y → P x → P y
disc≈ P {x}{y} e p = ind≈' (λ z p → P z) p e

inv≈ : {A : U} → {x y : A} → x ≈ y → y ≈ x
inv≈ {A}{x}{y} p = disc≈ (λ a → a ≈ x) p (refl x)

comp≈ : {A : U} → (x y z : A) → x ≈ y → y ≈ z → x ≈ z
comp≈ x y z p q = disc≈ (λ a → a ≈ z) (inv≈ p) q

infix 60 _·_
_·_ : {A : U} → {x y z : A} → x ≈ y → y ≈ z → x ≈ z
_·_ {A} {x} {y} {z} p q = comp≈ x y z p q

reflr≈ : {A : U} {x y : A} (p : x ≈ y) → p ≈ p · (refl y)
reflr≈ (refl x) = refl (refl x)

refll≈ : {A : U} {x y : A} (p : x ≈ y) → p ≈ (refl x) · p
refll≈ (refl x) = refl (refl x)

invl≈ : {A : U} {x y : A} (p : x ≈ y) → (inv≈ p) · p ≈ (refl y)
invl≈ (refl x) = refl (refl x)

invr≈ : {A : U} {x y : A} (p : x ≈ y) → p · (inv≈ p) ≈ (refl x)
invr≈ (refl x) = refl (refl x)

--path inversion is involutive
invinv≈ : {A : U} {x y : A} (p : x ≈ y) → (inv≈ (inv≈ p)) ≈ p
invinv≈ (refl x) = refl (refl x)

--associativity of path concatenation
assoc≈ : {A : U} {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) → p · (q · r) ≈ (p · q) · r
assoc≈ (refl x) (refl .x) (refl .x) = refl (refl x)

--natural numbers
data Nat : U where
  O : Nat
  S : Nat → Nat

--loop space
Ω : (A : U) → (a : A) → U
Ω A a = a ≈ a

--second order loop space
Ω2 : (A : U) → (a : A) → U
Ω2 A a = (refl a) ≈ (refl a)

--whiskering with constant right side
whiskerr : {A : U} {a b c : A} {p q : a ≈ b} → (α : p ≈ q) → (r : b ≈ c) → p · r ≈ q · r
whiskerr {A}{a}{b}{.b}{p}{q} α (refl .b) = (inv≈ (reflr≈ p) · α) · reflr≈ q

--whiskering with constant left side
whiskerl : {A : U} {a b c : A} → (q : a ≈ b) → {r s : b ≈ c} → (β : r ≈ s) → q · r ≈ q · s
whiskerl (refl a) {r}{s} β = ((inv≈ (refll≈ r) · β) · refll≈ s)

--horizontal composition
_⋆_ : {A : U} {a b c : A} {p q : a ≈ b} {r s : b ≈ c} → (α : p ≈ q) → (β : r ≈ s) → p · r ≈ q · s
_⋆_ {A}{a}{b}{c}{p}{q}{r}{s} α β = whiskerr α r · whiskerl q β

--horizontal composition, second version
_⋆'_ : {A : U} {a b c : A} {p q : a ≈ b} {r s : b ≈ c} → (α : p ≈ q) → (β : r ≈ s) → p · r ≈ q · s
_⋆'_ {A}{a}{b}{c}{p}{q}{r}{s} α β = whiskerl p β · whiskerr α s

--both definitions are equal
horiz≈ : {A : U} {a b c : A} {p q : a ≈ b} {r s : b ≈ c} → (α : p ≈ q) → (β : r ≈ s) → (α ⋆ β) ≈ (α ⋆' β)
--horiz≈ {A}{b}{.b}{.b}{refl .b}{refl .b}{refl .b}{s} (refl (refl .b)) (refl (refl .b)) = ?
horiz≈ {A}{a}{b}{c}{p}{q}{r}{s} α β = ind≈' (λ p α' → (α' ⋆ β) ≈ (α' ⋆' β))
                                     (ind≈' (λ r β' → (refl p ⋆ β') ≈ (refl p ⋆' β'))
                                     (ind≈' (λ b' r' → (refl p ⋆ refl r') ≈ (refl p ⋆' refl r'))
                                     (ind≈'' (λ a' p' → (refl p' ⋆ refl (refl b)) ≈ (refl p' ⋆' refl (refl b)))
                                     (refl (refl (refl b) ⋆ refl (refl b))) p) r) β) α

--for two-dimensional loops, horizontal composition equals 'vertical' composition
horiz-comp≈ : {A : U} {a : A} → (α β : Ω2 A a) → (α ⋆ β) ≈ (α · β)
horiz-comp≈ {A}{a} α β = ((refl (whiskerr α (refl a))) ⋆ (refl (whiskerl (refl a) β))) ·
                         (disc≈ (λ x → (x · (refl (refl a))) · (((inv≈ (refl (refl a))) · β) · (refl (refl a))) ≈ α · β) (refll≈ α)
                         (disc≈ (λ x → (α · refl (refl a)) · (x · refl (refl a)) ≈ α · β)                                (refll≈ β)
                         (disc≈ (λ x → x · (β · refl (refl a)) ≈ α · β)                                                  (reflr≈ α)
                         (disc≈ (λ x → α · x ≈ α · β)                                                                    (reflr≈ β)
                         (refl (α · β))))))

--for two-dimensional loops, the second way of horizontal composition equals composing vertically from left to right
horiz'-comp≈ : {A : U} {a : A} → (α β : Ω2 A a) → (α ⋆' β) ≈ (β · α)
horiz'-comp≈ {A}{a} α β = (refl (whiskerl (refl a) β) ⋆ refl (whiskerr α (refl a))) ·
                          (disc≈ (λ x → (x · (refl (refl a))) · (((inv≈ (refl (refl a))) · α) · (refl (refl a))) ≈ β · α) (refll≈ β)
                          (disc≈ (λ x → (β · refl (refl a)) · (x · refl (refl a)) ≈ β · α)                                (refll≈ α)
                          (disc≈ (λ x → x · (α · refl (refl a)) ≈ β · α)                                                  (reflr≈ β)
                          (disc≈ (λ x → β · x ≈ β · α)                                                                    (reflr≈ α)
                          (refl (β · α))))))

--Theorem 2.1.6: Eckmann-Hilton Argument
eckmann-hilton : (A : U) → (a : A) → (α β : Ω2 A a) → α · β ≈ β · α
eckmann-hilton A a α β = (inv≈ (horiz-comp≈ α β) · horiz≈ α β) · horiz'-comp≈ α β

data U* : U where
  pttype : (A : U) → A → U*

Ω*' : U* → U*
Ω*' (pttype A a) = pttype (a ≈ a) (refl a)

Ω* : Nat → U* → U*
Ω*     O (pttype A a) = pttype A a
Ω* (S n) A*           = Ω* n (Ω*' A*)

--Lemma 2.2.1: Functions are Fuctors
ap : {A B : U} → (f : A → B) → {x y : A} → x ≈ y → (f x) ≈ (f y)
ap f {x}{.x} (refl .x) = refl (f x)

--Lemma 2.2.2.i: Applying functions is itself functorial
apfunc : {A B : U} → (f : A → B) → {x y z : A} → (p : x ≈ y) → (q : y ≈ z) → ap f (p · q) ≈ (ap f p) · (ap f q)
apfunc f (refl x) (refl .x) = refl (refl (f x))

--Lemma 2.2.2.ii: Same with inverse paths
apinv : {A B : U} → (f : A → B) → {x y : A} → (p : x ≈ y) → ap f (inv≈ p) ≈ (inv≈ (ap f p))
apinv f (refl x) = refl (refl (f x))

_∘_ : {A B C : U} → (g : B → C) → (f : A → B) → (A → C)
(g ∘ f) a = g (f a)

--Lemma 2.2.2.iii: ... And with composed funcitons
apcomp : {A B C : U} → (f : A → B) → (g : B → C) → {x y : A} → (p : x ≈ y) → ap (g ∘ f) p ≈ ap g (ap f p)
apcomp f g {x}{.x} (refl .x) = refl (refl (g (f x)))

--Lemma 2.2.2.iv
apid : {A : U} → {x y : A} → (p : x ≈ y) → ap id p ≈ p
apid (refl x) = refl (refl x)

--Lemma 2.3.1
transport : {A : U} → (P : A → U) → {x y : A} → (p : x ≈ y) → P x → P y
transport P (refl x) = id

--Lemma 2.3.4
apd : {A : U} → {P : A → U} → (f : (x : A) → P x) → {x y : A} → (p : x ≈ y) → (transport P p (f x)) ≈ f y
apd f (refl x) = refl (f x)

--Lemma 2.3.5
transportconst : {A : U} → (B : U) → {x y : A} → (p : x ≈ y) → (b : B) → (transport (λ x → B) p b) ≈ b
transportconst B (refl x) b = refl b

--Lemma 2.3.8
apd-decomp : {A B : U} → (f : A → B) → {x y : A} → (p : x ≈ y) → (apd f p) ≈ (transportconst B p (f x)) · (ap f p)
apd-decomp f (refl x) = refl (refl (f x))

--Lemma 2.3.9
transport-comp : {A : U} → (P : A → U) → {x y z : A} → (p : x ≈ y) → (q : y ≈ z) → (u : P x)
  → (transport P q (transport P p u)) ≈ transport P (p · q) u
transport-comp P (refl x) (refl .x) u = refl u

--Lemma 2.3.10
transport-ap : {A B : U} → (f : A → B) → (P : B → U) → {x y : A} → (p : x ≈ y) → (u : P (f x))
  → (transport (P ∘ f) p u) ≈ transport P (ap f p) u
transport-ap f P (refl x) u = refl u

--Lemma 2.3.11
transport-family : {A : U} → (P Q : A → U) → (f : (x : A) → P x → Q x) → {x y : A} → (p : x ≈ y) → (u : P x)
  → (transport Q p (f x u)) ≈ f y (transport P p u)
transport-family P Q f (refl x) u = refl (f x u)

--Definition 2.4.1
_∼_ : {A : U} → {P : A → U} → (f g : (x : A) → P x) → U
_∼_ {A}{P} f g  = ((x : A) → f x ≈ g x)

--Lemma 2.4.2
refl∼ : {A : U} → {P : A → U} → (f : (x : A) → P x) → f ∼ f
refl∼ f x = refl (f x)

symm∼ : {A : U} → {P : A → U} → (f g : (x : A) → P x) → f ∼ g → g ∼ f
symm∼ f g H x = inv≈ (H x)

trans∼ : {A : U} → {P : A → U} → (f g h : (x : A) → P x) → f ∼ g → g ∼ h → f ∼ h
trans∼ f g h H H' x = H x · H' x

--Lemma 2.4.3
natural∼ : {A B : U} → {f g : A → B} → (H : f ∼ g) → {x y : A} → (p : x ≈ y) → (H x) · (ap g p) ≈ (ap f p) · (H y)
natural∼ H (refl x) = inv≈ (reflr≈ (H x)) · refll≈ (H x)

--Corollary 2.4.4
natural-null∼ : {A : U} → (f : A → A) → (H : f ∼ id) → (x : A) → H (f x) ≈ ap f (H x)
natural-null∼ f H x = reflr≈ (H (f x))
                    · (((refl (H (f x)) ⋆ inv≈ (invr≈ (H x))))
                    · (assoc≈ (H (f x)) (H x) (inv≈ (H x))
                    · (((refl (H (f x)) ⋆ inv≈ (apid (H x))) ⋆ refl (inv≈ (H x)))
                    · ((natural∼ H (H x) ⋆ refl (inv≈ (H x)))
                    · (inv≈ (assoc≈ (ap f (H x)) (H x) (inv≈ (H x)))
                    · ((refl (ap f (H x)) ⋆ invr≈ (H x))
                    · inv≈ (reflr≈ (ap f (H x)))))))))

--PRODUCT TYPE
infix 55 _×_
data _×_ : U → U → U where
  〈_,_〉 : {A B : U} → A → B → A × B

prl× : {A B : U} → A × B → A
prl× 〈 a , b 〉 = a

prr× : {A B : U} → A × B → B
prr× 〈 a , b 〉 = b

re× : {A B : U} → (s : A × B) → 〈 prl× s , prr× s 〉 ≈ s
re× 〈 a , b 〉 = refl 〈 a , b 〉

ind× : {A B : U} → (P : A × B → U) → ((a : A) → (b : B) → P 〈 a , b 〉) → (x : A × B) → P x
ind× P f 〈 a , b 〉 = f a b

--SIGMA TYPE
data Σ : {A : U} → (P : A → U) → U where
  ex : {A : U} → {P : A → U} → (a : A) → P a → Σ P

--induction on sigma type
--indΣ : {A : U} → {P : A → U} → Σ P → U
--indΣ {A}{P} = {!!}

--Definition 2.4indΣ.6
qinv : {A B : U} → (f : A → B) → U
qinv f = Σ (λ g → ((f ∘ g) ∼ id) × ((g ∘ f) ∼ id))

--Example 2.4.7
qinv-id : {A : U} → qinv (id {A})
qinv-id = ex id 〈 (λ x → refl x) , (λ x → refl x) 〉

--Example 2.4.8
qinv-postcomp : {A : U} → {x y : A} → (p : x ≈ y) → (z : A) → qinv (λ (q : y ≈ z) → p · q)
qinv-postcomp (refl x) z = ex (λ q → (refl x) · q) 〈 (λ x' → refl x') , (λ x' → refl x') 〉

qinv-precomp : {A : U} → {x y : A} → (p : x ≈ y) → (z : A) → qinv (λ (q : z ≈ x) → q · p)
qinv-precomp p z = ex (λ q → q · (inv≈ p)) 〈 (λ q' → inv≈ (assoc≈ q' (inv≈ p) p)
                                                    · ((refl q' ⋆ invl≈ p)
                                                    · inv≈ (reflr≈ q'))) ,
                                              (λ q' → inv≈ (assoc≈ q' p (inv≈ p))
                                                     · ((refl q' ⋆ invr≈ p)
                                                     · inv≈ (reflr≈ q'))) 〉

--Example 2.4.9
qinv-transport : {A : U} → {x y : A} → (P : A → U) → (p : x ≈ y) → qinv (transport P p)
qinv-transport P p = ex (transport P (inv≈ p)) 〈 (λ q → transport-comp P (inv≈ p) p q
                                                      · (ap (λ x → transport P x q) (invl≈ p)
                                                      · refl q)) ,
                                                 (λ q → transport-comp P p (inv≈ p) q
                                                       · (ap (λ x → transport P x q) (invr≈ p)
                                                       · refl q)) 〉

--ISEQUIV
isequiv : {A B : U} → (f : A → B) → U
isequiv f = (Σ (λ g → ((f ∘ g) ∼ id))) × (Σ (λ h → ((h ∘ f) ∼ id)))

prlΣ : {A : U} → {P : A → U} → Σ P → A
prlΣ (ex x y) = x

prrΣ : {A : U} → {P : A → U} → (x : Σ P) → P (prlΣ x)
prrΣ (ex x y) = y

qinv-isequiv : {A B : U} → (f : A → B) → qinv f → isequiv f
qinv-isequiv f x  = 〈 ex (prlΣ x) (prl× (prrΣ x)) , ex (prlΣ x) (prr× (prrΣ x)) 〉

--HORIZONTAL COMPOSITION FOR HOMOTOPIES
_⋆∼_ : {A B C : U} → {f f' : A → B} → {g g' : B → C} → (α : f ∼ f') → (β : g ∼ g') → (g ∘ f) ∼ (g' ∘ f')
_⋆∼_ {A}{B}{C}{f}{f'}{g}{g'} α β x = (ap g (α x)) · β (f' x)

--refll∼ : {A B : U} → {f f' : A → B} → (α : f ∼ f') →

isequiv-qinv : {A B : U} → (f : A → B) → isequiv f → qinv f
isequiv-qinv {A}{B} f eq = let g : B → A
                               g = prlΣ (prl× eq)
                               h : B → A
                               h = prlΣ (prr× eq)
                               α : (f ∘ g) ∼ id
                               α = prrΣ (prl× eq)
                               β : (h ∘ f) ∼ id
                               β = prrΣ (prr× eq)
                               γ : g ∼ h
                               γ x = inv≈ (β (g x)) · (ap h (α x))
                               β' : (g ∘ f) ∼ id
                               β' x = γ (f x) · β x
                           in ex g 〈 α , β' 〉

--HOMOTOPY EQUIVALENCE OF TYPES
_≃_ : (A B : U) → U
A ≃ B = Σ (λ (f : A → B) → isequiv f)

--Lemma 2.4.12.i: Reflexivity of Equivalence
refl≃ : (A : U) → A ≃ A
refl≃ A = ex id 〈 ex id (λ x → refl x) , ex id (λ x → refl x) 〉

--Lemma 2.4.12.ii: Symmetry of Equivalence
symm≃ : {A B : U} → A ≃ B → B ≃ A
symm≃ {A}{B} ev = let f : A → B
                      f = prlΣ ev
                      qi : qinv f
                      qi = isequiv-qinv f (prrΣ ev)
                      g : B → A
                      g = prlΣ qi
                      α : _
                      α = prl× (prrΣ qi)
                      β : _
                      β = prr× (prrΣ qi)
                  in ex g 〈 ex f β , ex f α 〉

--Lemma 2.4.12.iii: Transitivity of Equivalence
trans≃ : {A B C : U} → A ≃ B → B ≃ C → A ≃ C
trans≃ {A}{B}{C} ev1 ev2 = let f :  A → B
                               f = prlΣ ev1
                               qi1 = qinv f
                               qi1 = isequiv-qinv f (prrΣ ev1)
                               f' : B → A
                               f' = prlΣ qi1
                               αf : (f ∘ f') ∼ id
                               αf = prl× (prrΣ qi1)
                               βf : (f' ∘ f) ∼ id
                               βf = prr× (prrΣ qi1)
                               g : B → C
                               g = prlΣ ev2
                               qi2 = qinv g
                               qi2 = isequiv-qinv g (prrΣ ev2)
                               g' : C → B
                               g' = prlΣ qi2
                               αg : (g ∘ g') ∼ id
                               αg = prl× (prrΣ qi2)
                               βg : (g' ∘ g) ∼ id
                               βg = prr× (prrΣ qi2)
                           in ex (g ∘ f) 〈 ex (f' ∘ g') (λ c → ap g (αf (g' c)) · αg c) ,
                                           ex (f' ∘ g') (λ a → ap f'  (βg (f a)) · βf a) 〉

--Theorem 2.6.2
product≈-pr : {A B : U} → (x y : A × B) → (p : x ≈ y) → (prl× x ≈ prl× y) × (prr× x ≈ prr× y)
product≈-pr x y p = 〈 ap (λ x → prl× x) p , ap (λ x → prr× x) p 〉

pair≈ : {A B : U} → {x y : A × B} → (prl× x ≈ prl× y) × (prr× x ≈ prr× y) → x ≈ y
pair≈ {A}{B}{〈 a , b 〉}{〈 a' , b' 〉} pq = ind≈' (λ x' p → 〈 a , b 〉 ≈ 〈 x' , b' 〉)
                                      (ind≈' (λ y' p → 〈 a , b 〉 ≈ 〈 a , y' 〉)
                                             (refl 〈 a , b 〉) (prr× pq)) (prl× pq)

product≈-isequiv : {A B : U} → (x y : A × B) → isequiv (product≈-pr x y)
product≈-isequiv {A}{B} x y = qinv-isequiv (product≈-pr x y) (ex (pair≈) 〈 α x y , β x y 〉)
                       where α : (x y : A × B) → (product≈-pr x y ∘ pair≈) ∼ id
                             α 〈 a , b 〉 〈 a' , b' 〉 s =
                               ind≈' (λ x' p → (product≈-pr 〈 a , b 〉 〈 x' , b' 〉 ∘ pair≈) 〈 p , prr× s 〉 ≈ 〈 p , prr× s 〉)
                                     (ind≈' (λ x' p → (product≈-pr 〈 a , b 〉 〈 a , x' 〉 ∘ pair≈) 〈 refl a , p 〉 ≈ 〈 refl a , p 〉)
                                            (refl 〈 refl a , refl b 〉) (prr× s)) (prl× s) · re× s
                             β : (x y : A × B) → (pair≈ ∘ product≈-pr x y) ∼ id
                             β x y r =
                               ind≈' (λ y' p → (pair≈ ∘ product≈-pr x y') p ≈ p)
                                     (ind× (λ x' → (pair≈ ∘ product≈-pr x' x') (refl x') ≈ refl x')
                                           (λ a b → refl (refl 〈 a , b 〉)) x) r

--Theorem 2.6.4
transport-product : {Z : U} → (A B : Z → U) → {z w : Z} → (p : z ≈ w) → (x : A z × B z) →
  transport (λ z → A z × B z) p x ≈ 〈 transport A p (prl× x) , transport B p (prr× x) 〉
transport-product A B (refl z) x = inv≈ (re× x)

--Theorem 2.6.5
product-ap-functor : {A A' B B' : U} → (g : A → A') → (h : B → B') → (x y : A × B) → (p : prl× x ≈ prl× y) → (q : prr× x ≈ prr× y) →
  ap (λ x → 〈 g (prl× x) , h (prr× x) 〉) (pair≈ {A}{B}{x}{y} 〈 p , q 〉) ≈ pair≈ 〈 ap g p , ap h q 〉
product-ap-functor {A}{A'}{B}{B'} g h 〈 .a , .b 〉 〈 .a , .b 〉 (refl a) (refl b) = refl (refl 〈 g a , h b 〉)

--TRANSPORT EQUALITY ALONG SIGMA TYPE


--Theorem 2.7.2
Σ≈-decomp : {A : U} → {P : A → U} → (w w' : Σ P)
  → (w ≈ w') ≃ Σ (λ (p : prlΣ w ≈ prlΣ w') → transport P p (prrΣ w) ≈ prrΣ w')
Σ≈-decomp {A}{P} w w' = ex (f w w') (qinv-isequiv (f w w') (ex (g w w') 〈 α w w' , β w w' 〉))
  where f : (w w' : Σ P) → w ≈ w' → Σ (λ p → transport P p (prrΣ w) ≈ prrΣ w')
        f w w' p = ind≈' (λ w'' p' → Σ (λ p0 → transport P p0 (prrΣ w) ≈ prrΣ w''))
                         (ex (refl (prlΣ w)) (refl (prrΣ w))) p
        g : (w w' : Σ P) → Σ (λ p → transport P p (prrΣ w) ≈ prrΣ w') → w ≈ w'
        g (ex w1 w2) (ex w1' w2') exi = ind≈' (λ w1'' p' → ex w1 w2 ≈ ex w1'' (transport P p' w2))
                                              (refl (ex w1 w2)) p · ap (λ x → ex w1' x) q
          where p : w1 ≈ w1'
                p = prlΣ exi
                q : transport P p w2 ≈ w2'
                q = prrΣ exi
        α : (w w' : Σ P) → (f w w' ∘ g w w') ∼ id
        α (ex w1 w2) (ex w1' w2') exi = {!!}
          where p : w1 ≈ w1'
                p = prlΣ exi
                q : transport P p w2 ≈ w2'
                q = prrΣ exi
        β : (w w' : Σ P) → (g w w' ∘ f w w') ∼ id
        β x = {!!}
	{-# OPTIONS --type-in-type --without-K #-}

	module HoTT where

	U = Set4

	data Zero : U where

	data One : U where
	star : One

	data Two : U where
	starone : Two
	startwo : Two

	Not : U → U
	Not A = (A → Zero)

	notnot : (A : U) → A → Not (Not A)
	notnot A a f = f a

	notnotnot : (A : U) → Not (Not (Not A)) → Not A
	notnotnot A f a = f (notnot A a)

	data _+_ : U → U → U where
	inl : {A B : U} → A → A + B
	inr : {A B : U} → B → A + B

	rec+ : (A B C : U) → (A → C) → (B → C) → (A + B) → C
	rec+ A B C f g (inl a) = f a
	rec+ A B C f g (inr b) = g b

	restrl : {A B C : U} → ((A + B) → C) → A → C
	restrl f a = f (inl a)

	restrr : {A B C : U} → ((A + B) → C) → B → C
	restrr f b = f (inr b)

	notnotlem : (A : U) → Not (Not ((Not A) + A))
	notnotlem A f = f (inl (restrr f))

	id : {A : U} → A → A
	id x = x

	swap : {A B C : U} → (A → B → C) → B → A → C
	swap f b a = f a b

	data _≈_ : {A : U} → A → A → U where
	refl : {A : U} → (x : A) → (x ≈ x)

	ind≈ : {A : U} (C : (x y : A) → (x ≈ y) → U) → ((x : A) → C x x (refl x)) → {x y : A} (p : x ≈ y) → C x y p
	ind≈ C c (refl x) = c x

	ind≈' : {A : U} {a : A} (C : ((x : A) → a ≈ x → U)) → C a (refl a) → {x : A} (p : a ≈ x) → C x p
	ind≈' {A}{a} C c {.a} (refl .a) = c

	ind≈'' : {A : U} {a : A} (C : ((x : A) → x ≈ a → U)) → C a (refl a) → {x : A} (p : x ≈ a) → C x p
	ind≈'' {A}{a} C c {.a} (refl .a) = c

	disc≈ : {A : U} → (P : A → U) → {x y : A} → x ≈ y → P x → P y
	disc≈ P {x}{y} e p = ind≈' (λ z p → P z) p e

	inv≈ : {A : U} → {x y : A} → x ≈ y → y ≈ x
	inv≈ {A}{x}{y} p = disc≈ (λ a → a ≈ x) p (refl x)

	comp≈ : {A : U} → (x y z : A) → x ≈ y → y ≈ z → x ≈ z
	comp≈ x y z p q = disc≈ (λ a → a ≈ z) (inv≈ p) q

	infix 60 _·_
	_·_ : {A : U} → {x y z : A} → x ≈ y → y ≈ z → x ≈ z
	_·_ {A} {x} {y} {z} p q = comp≈ x y z p q

	reflr≈ : {A : U} {x y : A} (p : x ≈ y) → p ≈ p · (refl y)
	reflr≈ (refl x) = refl (refl x)

	refll≈ : {A : U} {x y : A} (p : x ≈ y) → p ≈ (refl x) · p
	refll≈ (refl x) = refl (refl x)

	invl≈ : {A : U} {x y : A} (p : x ≈ y) → (inv≈ p) · p ≈ (refl y)
	invl≈ (refl x) = refl (refl x)

	invr≈ : {A : U} {x y : A} (p : x ≈ y) → p · (inv≈ p) ≈ (refl x)
	invr≈ (refl x) = refl (refl x)

	--path inversion is involutive
	invinv≈ : {A : U} {x y : A} (p : x ≈ y) → (inv≈ (inv≈ p)) ≈ p
	invinv≈ (refl x) = refl (refl x)

	--associativity of path concatenation
	assoc≈ : {A : U} {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) → p · (q · r) ≈ (p · q) · r
	assoc≈ (refl x) (refl .x) (refl .x) = refl (refl x)

	--natural numbers
	data Nat : U where
	O : Nat
	S : Nat → Nat

	--loop space
	Ω : (A : U) → (a : A) → U
	Ω A a = a ≈ a

	--second order loop space
	Ω2 : (A : U) → (a : A) → U
	Ω2 A a = (refl a) ≈ (refl a)

	--whiskering with constant right side
	whiskerr : {A : U} {a b c : A} {p q : a ≈ b} → (α : p ≈ q) → (r : b ≈ c) → p · r ≈ q · r
	whiskerr {A}{a}{b}{.b}{p}{q} α (refl .b) = (inv≈ (reflr≈ p) · α) · reflr≈ q

	--whiskering with constant left side
	whiskerl : {A : U} {a b c : A} → (q : a ≈ b) → {r s : b ≈ c} → (β : r ≈ s) → q · r ≈ q · s
	whiskerl (refl a) {r}{s} β = ((inv≈ (refll≈ r) · β) · refll≈ s)

	--horizontal composition
	_⋆_ : {A : U} {a b c : A} {p q : a ≈ b} {r s : b ≈ c} → (α : p ≈ q) → (β : r ≈ s) → p · r ≈ q · s
	_⋆_ {A}{a}{b}{c}{p}{q}{r}{s} α β = whiskerr α r · whiskerl q β

	--horizontal composition, second version
	_⋆'_ : {A : U} {a b c : A} {p q : a ≈ b} {r s : b ≈ c} → (α : p ≈ q) → (β : r ≈ s) → p · r ≈ q · s
	_⋆'_ {A}{a}{b}{c}{p}{q}{r}{s} α β = whiskerl p β · whiskerr α s

	--both definitions are equal
	horiz≈ : {A : U} {a b c : A} {p q : a ≈ b} {r s : b ≈ c} → (α : p ≈ q) → (β : r ≈ s) → (α ⋆ β) ≈ (α ⋆' β)
	--horiz≈ {A}{b}{.b}{.b}{refl .b}{refl .b}{refl .b}{s} (refl (refl .b)) (refl (refl .b)) = ?
	horiz≈ {A}{a}{b}{c}{p}{q}{r}{s} α β = ind≈' (λ p α' → (α' ⋆ β) ≈ (α' ⋆' β))
	(ind≈' (λ r β' → (refl p ⋆ β') ≈ (refl p ⋆' β'))
	(ind≈' (λ b' r' → (refl p ⋆ refl r') ≈ (refl p ⋆' refl r'))
	(ind≈'' (λ a' p' → (refl p' ⋆ refl (refl b)) ≈ (refl p' ⋆' refl (refl b)))
	(refl (refl (refl b) ⋆ refl (refl b))) p) r) β) α

	--for two-dimensional loops, horizontal composition equals 'vertical' composition
	horiz-comp≈ : {A : U} {a : A} → (α β : Ω2 A a) → (α ⋆ β) ≈ (α · β)
	horiz-comp≈ {A}{a} α β = ((refl (whiskerr α (refl a))) ⋆ (refl (whiskerl (refl a) β))) ·
	(disc≈ (λ x → (x · (refl (refl a))) · (((inv≈ (refl (refl a))) · β) · (refl (refl a))) ≈ α · β) (refll≈ α)
	(disc≈ (λ x → (α · refl (refl a)) · (x · refl (refl a)) ≈ α · β) (refll≈ β)
	(disc≈ (λ x → x · (β · refl (refl a)) ≈ α · β) (reflr≈ α)
	(disc≈ (λ x → α · x ≈ α · β) (reflr≈ β)
	(refl (α · β))))))

	--for two-dimensional loops, the second way of horizontal composition equals composing vertically from left to right
	horiz'-comp≈ : {A : U} {a : A} → (α β : Ω2 A a) → (α ⋆' β) ≈ (β · α)
	horiz'-comp≈ {A}{a} α β = (refl (whiskerl (refl a) β) ⋆ refl (whiskerr α (refl a))) ·
	(disc≈ (λ x → (x · (refl (refl a))) · (((inv≈ (refl (refl a))) · α) · (refl (refl a))) ≈ β · α) (refll≈ β)
	(disc≈ (λ x → (β · refl (refl a)) · (x · refl (refl a)) ≈ β · α) (refll≈ α)
	(disc≈ (λ x → x · (α · refl (refl a)) ≈ β · α) (reflr≈ β)
	(disc≈ (λ x → β · x ≈ β · α) (reflr≈ α)
	(refl (β · α))))))

	--Theorem 2.1.6: Eckmann-Hilton Argument
	eckmann-hilton : (A : U) → (a : A) → (α β : Ω2 A a) → α · β ≈ β · α
	eckmann-hilton A a α β = (inv≈ (horiz-comp≈ α β) · horiz≈ α β) · horiz'-comp≈ α β

	data U* : U where
	pttype : (A : U) → A → U*

	Ω' : U → U*
	Ω*' (pttype A a) = pttype (a ≈ a) (refl a)

	Ω* : Nat → U* → U*
	Ω* O (pttype A a) = pttype A a
	Ω* (S n) A* = Ω* n (Ω' A)

	--Lemma 2.2.1: Functions are Fuctors
	ap : {A B : U} → (f : A → B) → {x y : A} → x ≈ y → (f x) ≈ (f y)
	ap f {x}{.x} (refl .x) = refl (f x)

	--Lemma 2.2.2.i: Applying functions is itself functorial
	apfunc : {A B : U} → (f : A → B) → {x y z : A} → (p : x ≈ y) → (q : y ≈ z) → ap f (p · q) ≈ (ap f p) · (ap f q)
	apfunc f (refl x) (refl .x) = refl (refl (f x))

	--Lemma 2.2.2.ii: Same with inverse paths
	apinv : {A B : U} → (f : A → B) → {x y : A} → (p : x ≈ y) → ap f (inv≈ p) ≈ (inv≈ (ap f p))
	apinv f (refl x) = refl (refl (f x))

	_∘_ : {A B C : U} → (g : B → C) → (f : A → B) → (A → C)
	(g ∘ f) a = g (f a)

	--Lemma 2.2.2.iii: ... And with composed funcitons
	apcomp : {A B C : U} → (f : A → B) → (g : B → C) → {x y : A} → (p : x ≈ y) → ap (g ∘ f) p ≈ ap g (ap f p)
	apcomp f g {x}{.x} (refl .x) = refl (refl (g (f x)))

	--Lemma 2.2.2.iv
	apid : {A : U} → {x y : A} → (p : x ≈ y) → ap id p ≈ p
	apid (refl x) = refl (refl x)

	--Lemma 2.3.1
	transport : {A : U} → (P : A → U) → {x y : A} → (p : x ≈ y) → P x → P y
	transport P (refl x) = id

	--Lemma 2.3.4
	apd : {A : U} → {P : A → U} → (f : (x : A) → P x) → {x y : A} → (p : x ≈ y) → (transport P p (f x)) ≈ f y
	apd f (refl x) = refl (f x)

	--Lemma 2.3.5
	transportconst : {A : U} → (B : U) → {x y : A} → (p : x ≈ y) → (b : B) → (transport (λ x → B) p b) ≈ b
	transportconst B (refl x) b = refl b

	--Lemma 2.3.8
	apd-decomp : {A B : U} → (f : A → B) → {x y : A} → (p : x ≈ y) → (apd f p) ≈ (transportconst B p (f x)) · (ap f p)
	apd-decomp f (refl x) = refl (refl (f x))

	--Lemma 2.3.9
	transport-comp : {A : U} → (P : A → U) → {x y z : A} → (p : x ≈ y) → (q : y ≈ z) → (u : P x)
	→ (transport P q (transport P p u)) ≈ transport P (p · q) u
	transport-comp P (refl x) (refl .x) u = refl u

	--Lemma 2.3.10
	transport-ap : {A B : U} → (f : A → B) → (P : B → U) → {x y : A} → (p : x ≈ y) → (u : P (f x))
	→ (transport (P ∘ f) p u) ≈ transport P (ap f p) u
	transport-ap f P (refl x) u = refl u

	--Lemma 2.3.11
	transport-family : {A : U} → (P Q : A → U) → (f : (x : A) → P x → Q x) → {x y : A} → (p : x ≈ y) → (u : P x)
	→ (transport Q p (f x u)) ≈ f y (transport P p u)
	transport-family P Q f (refl x) u = refl (f x u)

	--Definition 2.4.1
	_∼_ : {A : U} → {P : A → U} → (f g : (x : A) → P x) → U
	_∼_ {A}{P} f g = ((x : A) → f x ≈ g x)

	--Lemma 2.4.2
	refl∼ : {A : U} → {P : A → U} → (f : (x : A) → P x) → f ∼ f
	refl∼ f x = refl (f x)

	symm∼ : {A : U} → {P : A → U} → (f g : (x : A) → P x) → f ∼ g → g ∼ f
	symm∼ f g H x = inv≈ (H x)

	trans∼ : {A : U} → {P : A → U} → (f g h : (x : A) → P x) → f ∼ g → g ∼ h → f ∼ h
	trans∼ f g h H H' x = H x · H' x

	--Lemma 2.4.3
	natural∼ : {A B : U} → {f g : A → B} → (H : f ∼ g) → {x y : A} → (p : x ≈ y) → (H x) · (ap g p) ≈ (ap f p) · (H y)
	natural∼ H (refl x) = inv≈ (reflr≈ (H x)) · refll≈ (H x)

	--Corollary 2.4.4
	natural-null∼ : {A : U} → (f : A → A) → (H : f ∼ id) → (x : A) → H (f x) ≈ ap f (H x)
	natural-null∼ f H x = reflr≈ (H (f x))
	· (((refl (H (f x)) ⋆ inv≈ (invr≈ (H x))))
	· (assoc≈ (H (f x)) (H x) (inv≈ (H x))
	· (((refl (H (f x)) ⋆ inv≈ (apid (H x))) ⋆ refl (inv≈ (H x)))
	· ((natural∼ H (H x) ⋆ refl (inv≈ (H x)))
	· (inv≈ (assoc≈ (ap f (H x)) (H x) (inv≈ (H x)))
	· ((refl (ap f (H x)) ⋆ invr≈ (H x))
	· inv≈ (reflr≈ (ap f (H x)))))))))

	--PRODUCT TYPE
	infix 55 _×_
	data _×_ : U → U → U where
	〈_,_〉 : {A B : U} → A → B → A × B

	prl× : {A B : U} → A × B → A
	prl× 〈 a , b 〉 = a

	prr× : {A B : U} → A × B → B
	prr× 〈 a , b 〉 = b

	re× : {A B : U} → (s : A × B) → 〈 prl× s , prr× s 〉 ≈ s
	re× 〈 a , b 〉 = refl 〈 a , b 〉

	ind× : {A B : U} → (P : A × B → U) → ((a : A) → (b : B) → P 〈 a , b 〉) → (x : A × B) → P x
	ind× P f 〈 a , b 〉 = f a b

	--SIGMA TYPE
	data Σ : {A : U} → (P : A → U) → U where
	ex : {A : U} → {P : A → U} → (a : A) → P a → Σ P

	--induction on sigma type
	--indΣ : {A : U} → {P : A → U} → Σ P → U
	--indΣ {A}{P} = {!!}

	--Definition 2.4indΣ.6
	qinv : {A B : U} → (f : A → B) → U
	qinv f = Σ (λ g → ((f ∘ g) ∼ id) × ((g ∘ f) ∼ id))

	--Example 2.4.7
	qinv-id : {A : U} → qinv (id {A})
	qinv-id = ex id 〈 (λ x → refl x) , (λ x → refl x) 〉

	--Example 2.4.8
	qinv-postcomp : {A : U} → {x y : A} → (p : x ≈ y) → (z : A) → qinv (λ (q : y ≈ z) → p · q)
	qinv-postcomp (refl x) z = ex (λ q → (refl x) · q) 〈 (λ x' → refl x') , (λ x' → refl x') 〉

	qinv-precomp : {A : U} → {x y : A} → (p : x ≈ y) → (z : A) → qinv (λ (q : z ≈ x) → q · p)
	qinv-precomp p z = ex (λ q → q · (inv≈ p)) 〈 (λ q' → inv≈ (assoc≈ q' (inv≈ p) p)
	· ((refl q' ⋆ invl≈ p)
	· inv≈ (reflr≈ q'))) ,
	(λ q' → inv≈ (assoc≈ q' p (inv≈ p))
	· ((refl q' ⋆ invr≈ p)
	· inv≈ (reflr≈ q'))) 〉

	--Example 2.4.9
	qinv-transport : {A : U} → {x y : A} → (P : A → U) → (p : x ≈ y) → qinv (transport P p)
	qinv-transport P p = ex (transport P (inv≈ p)) 〈 (λ q → transport-comp P (inv≈ p) p q
	· (ap (λ x → transport P x q) (invl≈ p)
	· refl q)) ,
	(λ q → transport-comp P p (inv≈ p) q
	· (ap (λ x → transport P x q) (invr≈ p)
	· refl q)) 〉

	--ISEQUIV
	isequiv : {A B : U} → (f : A → B) → U
	isequiv f = (Σ (λ g → ((f ∘ g) ∼ id))) × (Σ (λ h → ((h ∘ f) ∼ id)))

	prlΣ : {A : U} → {P : A → U} → Σ P → A
	prlΣ (ex x y) = x

	prrΣ : {A : U} → {P : A → U} → (x : Σ P) → P (prlΣ x)
	prrΣ (ex x y) = y

	qinv-isequiv : {A B : U} → (f : A → B) → qinv f → isequiv f
	qinv-isequiv f x = 〈 ex (prlΣ x) (prl× (prrΣ x)) , ex (prlΣ x) (prr× (prrΣ x)) 〉

	--HORIZONTAL COMPOSITION FOR HOMOTOPIES
	_⋆∼_ : {A B C : U} → {f f' : A → B} → {g g' : B → C} → (α : f ∼ f') → (β : g ∼ g') → (g ∘ f) ∼ (g' ∘ f')
	_⋆∼_ {A}{B}{C}{f}{f'}{g}{g'} α β x = (ap g (α x)) · β (f' x)

	--refll∼ : {A B : U} → {f f' : A → B} → (α : f ∼ f') →

	isequiv-qinv : {A B : U} → (f : A → B) → isequiv f → qinv f
	isequiv-qinv {A}{B} f eq = let g : B → A
	g = prlΣ (prl× eq)
	h : B → A
	h = prlΣ (prr× eq)
	α : (f ∘ g) ∼ id
	α = prrΣ (prl× eq)
	β : (h ∘ f) ∼ id
	β = prrΣ (prr× eq)
	γ : g ∼ h
	γ x = inv≈ (β (g x)) · (ap h (α x))
	β' : (g ∘ f) ∼ id
	β' x = γ (f x) · β x
	in ex g 〈 α , β' 〉

	--HOMOTOPY EQUIVALENCE OF TYPES
	_≃_ : (A B : U) → U
	A ≃ B = Σ (λ (f : A → B) → isequiv f)

	--Lemma 2.4.12.i: Reflexivity of Equivalence
	refl≃ : (A : U) → A ≃ A
	refl≃ A = ex id 〈 ex id (λ x → refl x) , ex id (λ x → refl x) 〉

	--Lemma 2.4.12.ii: Symmetry of Equivalence
	symm≃ : {A B : U} → A ≃ B → B ≃ A
	symm≃ {A}{B} ev = let f : A → B
	f = prlΣ ev
	qi : qinv f
	qi = isequiv-qinv f (prrΣ ev)
	g : B → A
	g = prlΣ qi
	α : _
	α = prl× (prrΣ qi)
	β : _
	β = prr× (prrΣ qi)
	in ex g 〈 ex f β , ex f α 〉

	--Lemma 2.4.12.iii: Transitivity of Equivalence
	trans≃ : {A B C : U} → A ≃ B → B ≃ C → A ≃ C
	trans≃ {A}{B}{C} ev1 ev2 = let f : A → B
	f = prlΣ ev1
	qi1 = qinv f
	qi1 = isequiv-qinv f (prrΣ ev1)
	f' : B → A
	f' = prlΣ qi1
	αf : (f ∘ f') ∼ id
	αf = prl× (prrΣ qi1)
	βf : (f' ∘ f) ∼ id
	βf = prr× (prrΣ qi1)
	g : B → C
	g = prlΣ ev2
	qi2 = qinv g
	qi2 = isequiv-qinv g (prrΣ ev2)
	g' : C → B
	g' = prlΣ qi2
	αg : (g ∘ g') ∼ id
	αg = prl× (prrΣ qi2)
	βg : (g' ∘ g) ∼ id
	βg = prr× (prrΣ qi2)
	in ex (g ∘ f) 〈 ex (f' ∘ g') (λ c → ap g (αf (g' c)) · αg c) ,
	ex (f' ∘ g') (λ a → ap f' (βg (f a)) · βf a) 〉

	--Theorem 2.6.2
	product≈-pr : {A B : U} → (x y : A × B) → (p : x ≈ y) → (prl× x ≈ prl× y) × (prr× x ≈ prr× y)
	product≈-pr x y p = 〈 ap (λ x → prl× x) p , ap (λ x → prr× x) p 〉

	pair≈ : {A B : U} → {x y : A × B} → (prl× x ≈ prl× y) × (prr× x ≈ prr× y) → x ≈ y
	pair≈ {A}{B}{〈 a , b 〉}{〈 a' , b' 〉} pq = ind≈' (λ x' p → 〈 a , b 〉 ≈ 〈 x' , b' 〉)
	(ind≈' (λ y' p → 〈 a , b 〉 ≈ 〈 a , y' 〉)
	(refl 〈 a , b 〉) (prr× pq)) (prl× pq)

	product≈-isequiv : {A B : U} → (x y : A × B) → isequiv (product≈-pr x y)
	product≈-isequiv {A}{B} x y = qinv-isequiv (product≈-pr x y) (ex (pair≈) 〈 α x y , β x y 〉)
	where α : (x y : A × B) → (product≈-pr x y ∘ pair≈) ∼ id
	α 〈 a , b 〉 〈 a' , b' 〉 s =
	ind≈' (λ x' p → (product≈-pr 〈 a , b 〉 〈 x' , b' 〉 ∘ pair≈) 〈 p , prr× s 〉 ≈ 〈 p , prr× s 〉)
	(ind≈' (λ x' p → (product≈-pr 〈 a , b 〉 〈 a , x' 〉 ∘ pair≈) 〈 refl a , p 〉 ≈ 〈 refl a , p 〉)
	(refl 〈 refl a , refl b 〉) (prr× s)) (prl× s) · re× s
	β : (x y : A × B) → (pair≈ ∘ product≈-pr x y) ∼ id
	β x y r =
	ind≈' (λ y' p → (pair≈ ∘ product≈-pr x y') p ≈ p)
	(ind× (λ x' → (pair≈ ∘ product≈-pr x' x') (refl x') ≈ refl x')
	(λ a b → refl (refl 〈 a , b 〉)) x) r

	--Theorem 2.6.4
	transport-product : {Z : U} → (A B : Z → U) → {z w : Z} → (p : z ≈ w) → (x : A z × B z) →
	transport (λ z → A z × B z) p x ≈ 〈 transport A p (prl× x) , transport B p (prr× x) 〉
	transport-product A B (refl z) x = inv≈ (re× x)

	--Theorem 2.6.5
	product-ap-functor : {A A' B B' : U} → (g : A → A') → (h : B → B') → (x y : A × B) → (p : prl× x ≈ prl× y) → (q : prr× x ≈ prr× y) →
	ap (λ x → 〈 g (prl× x) , h (prr× x) 〉) (pair≈ {A}{B}{x}{y} 〈 p , q 〉) ≈ pair≈ 〈 ap g p , ap h q 〉
	product-ap-functor {A}{A'}{B}{B'} g h 〈 .a , .b 〉 〈 .a , .b 〉 (refl a) (refl b) = refl (refl 〈 g a , h b 〉)

	--TRANSPORT EQUALITY ALONG SIGMA TYPE


	--Theorem 2.7.2
	Σ≈-decomp : {A : U} → {P : A → U} → (w w' : Σ P)
	→ (w ≈ w') ≃ Σ (λ (p : prlΣ w ≈ prlΣ w') → transport P p (prrΣ w) ≈ prrΣ w')
	Σ≈-decomp {A}{P} w w' = ex (f w w') (qinv-isequiv (f w w') (ex (g w w') 〈 α w w' , β w w' 〉))
	where f : (w w' : Σ P) → w ≈ w' → Σ (λ p → transport P p (prrΣ w) ≈ prrΣ w')
	f w w' p = ind≈' (λ w'' p' → Σ (λ p0 → transport P p0 (prrΣ w) ≈ prrΣ w''))
	(ex (refl (prlΣ w)) (refl (prrΣ w))) p
	g : (w w' : Σ P) → Σ (λ p → transport P p (prrΣ w) ≈ prrΣ w') → w ≈ w'
	g (ex w1 w2) (ex w1' w2') exi = ind≈' (λ w1'' p' → ex w1 w2 ≈ ex w1'' (transport P p' w2))
	(refl (ex w1 w2)) p · ap (λ x → ex w1' x) q
	where p : w1 ≈ w1'
	p = prlΣ exi
	q : transport P p w2 ≈ w2'
	q = prrΣ exi
	α : (w w' : Σ P) → (f w w' ∘ g w w') ∼ id
	α (ex w1 w2) (ex w1' w2') exi = {!!}
	where p : w1 ≈ w1'
	p = prlΣ exi
	q : transport P p w2 ≈ w2'
	q = prrΣ exi
	β : (w w' : Σ P) → (g w w' ∘ f w w') ∼ id
	β x = {!!}