smth.agda

open import Agda.Primitive

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

cong : {a b : Level} {A : Set a} {B : Set b} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

sym : {a : Level} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {a : Level} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

subst : {a b : Level}{A : Set a}{x y : A}(_ : x ≡ y)(P : A → Set b) → P x → P y
subst refl P i = i

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B

open _×_ public

path : {a : Level} {A : Set a} (x y : A) → Set (lsuc a)
path {a} {A} x y = (P : A → Set a) → P x → P y

id_fun : {a : Level}{T : Set a}(_ : T) → T
id_fun i = i

id-path : {a : Level} {A : Set a} (i : A) → path i i
id-path i P = id_fun

is-center : {a : Level} {T : Set a} (v : T) → Set a
is-center {a} {T} v = (i : T) → i ≡ v

is-contr : {a : Level} (T : Set a) → Set a
is-contr T = Σ T is-center

contr-ty-vals-irrel : {a : Level} {T : Set a} (c : is-contr T) (x y : T) → x ≡ y
contr-ty-vals-irrel c x y = trans (snd c x) (sym (snd c y))

wmap : {a b : Level} (A : Set a) (B : Set b) → Set (a ⊔ b)
wmap A B = Σ ((A → B) × (B → A)) (λ p → (i : A) → snd p (fst p i) ≡ i)

mkwmap : {a b : Level} {A : Set a} {B : Set b} (f : A → B) (h : B → A) (p : (i : A) → h (f i) ≡ i) → wmap A B
mkwmap f h p = ((f , h) , p)

eq-to-path : {a : Level} {A : Set a} {x y : A} → x ≡ y → path x y
eq-to-path {x = x} refl = id-path x

postulate
  funext : {a b : Level} {A : Set a} {B : A → Set b} {f g : (x : A) → B x}
        → ((x : A) → f x ≡ g x) → f ≡ g

h437-2 : {a b : Level} {A : Set a} {B : Set b} (re : wmap B A) (c : is-contr A) → is-contr B
h437-2 (((r , s) , eps)) (a , p) = 
    s a , λ y → trans (sym (eps y)) (cong s (p (r y)))

eq-contr : {a : Level} {A : Set a} {x : A} → is-contr (x ≡ x)
eq-contr = refl , λ { refl → refl }

mutual
    path-is-eq-p : {a : Level} {A : Set a} (x y : A) → wmap (path x y) (x ≡ y)
    path-is-eq-p x y = mkwmap 
        (λ k → k (λ i → x ≡ i) refl)
        eq-to-path 
        (path-is-eq-p-cancel x y)

    path-is-eq-p-cancel : {a : Level} {A : Set a} (x y : A) (p : path x y)
        → eq-to-path (p (λ i → x ≡ i) refl) ≡ p

    path-is-eq-p-cancel {a = a} {A = A} x y p =
        funext (λ P → funext (λ u → loop (p (λ i → x ≡ i) refl) P u))
        where
        loop : (j : x ≡ y) (P : A → Set a) (u : P x) → eq-to-path j P u ≡ p P u
        loop refl P u = 
            sym (cong (λ i → i P u) (parm p))

    path-contr : {a : Level} {A : Set a} (i : A) → is-contr (path i i)
    path-contr i = h437-2 (path-is-eq-p i i) eq-contr


    parm : {a : Level} {A : Set a} {i : A} (p : path i i) → p ≡ id-path i
    parm {a} {A} {i} p = contr-ty-vals-irrel (path-contr i) p (id-path i)