```{-# OPTIONS --without-K #-}
module hott.equivalence.inverse where

open import level
open import sum
open import function.core
open import function.isomorphism.core
open import function.isomorphism.utils
open import function.isomorphism.properties
open import function.extensionality
open import equality.core
open import sets.unit
open import sets.nat.core using (suc)
open import hott.level
open import hott.equivalence.core
open import hott.equivalence.alternative
open import hott.univalence

module _ {i j}{A : Set i}{B : Set j} where
record inverse (f : A → B) : Set (i ⊔ j) where
constructor mk-inverse
field
g : B → A
α : (x : A) → g (f x) ≡ x
β : (y : B) → f (g y) ≡ y

isom : A ≅ B
isom = iso f g α β

iso⇒inv : (f : A ≅ B) → inverse (apply f)
iso⇒inv (iso f g α β) = mk-inverse g α β

inverse-struct-iso : (f : A → B)
→ inverse f
≅ ( Σ (B → A) λ g
→ Σ ((x : A) → g (f x) ≡ x) λ α
→ ((y : B) → f (g y) ≡ y) )
inverse-struct-iso f = record
{ to = λ { (mk-inverse g α β) → (g , α , β) }
; from = λ { (g , α , β) → (mk-inverse g α β) }
; iso₁ = λ _ → refl
; iso₂ = λ _ → refl }

≅-inv-struct-iso : (A ≅ B) ≅ Σ (A → B) inverse
≅-inv-struct-iso = trans≅ ≅-struct-iso
(Σ-ap-iso₂ (λ f → sym≅ (inverse-struct-iso f)))

ind-≈ : (P : ∀ {i}{A B : Set i} → A ≈ B → Set i)
→ (∀ {i}{A : Set i} → P {A = A} (≡⇒≈ refl))
→ ∀ {i}{A B : Set i}(eq : A ≈ B) → P eq
ind-≈ P d {A = A} eq = subst P (_≅_.iso₂ uni-iso eq)
(lem (≈⇒≡ eq))
where
lem : ∀ {i}{A B : Set i}
→ (p : A ≡ B)
→ P (≡⇒≈ p)
lem refl = d

inverse-nonprop' : ∀ {i}{A : Set i}
→ inverse (λ (x : A) → x)
≅ ((x : A) → x ≡ x)
inverse-nonprop' {i}{A} = begin
inverse id'
≅⟨ inverse-struct-iso id' ⟩
( Σ (A → A) λ g
→ Σ ((x : A) → g x ≡ x) λ α
→ ((y : A) → g y  ≡ y) )
≅⟨ ( Σ-ap-iso₂ λ g
→ Σ-ap-iso₁ strong-funext-iso ) ⟩
( Σ (A → A) λ g
→ Σ (g ≡ id') λ α
→ ((y : A) → g y ≡ y) )
≅⟨ sym≅ Σ-assoc-iso ⟩
( Σ (singleton' id') λ { (g , α)
→ ((y : A) → g y ≡ y) } )
≅⟨ trans≅ (Σ-ap-iso' (contr-⊤-iso (singl-contr' id'))
(λ _ → refl≅))
×-left-unit ⟩
((x : A) → x ≡ x)
∎
where
open ≅-Reasoning
id' : A → A
id' x = x

inverse-nonprop : ∀ {i}{A B : Set i}
→ (f : A → B)
→ weak-equiv f
→ inverse f
≅ ((x : A) → x ≡ x)
inverse-nonprop {i}{A} f we = ind-≈ P inverse-nonprop' (f , we)
where
P : ∀ {i}{A B : Set i} → A ≈ B → Set _
P {A = A} (f , we) = inverse f ≅ ((x : A) → x ≡ x)

```