-- This module closely follows a section of Martín Escardó's HoTT lecture notes:
-- https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#equivalenceinduction
{-# OPTIONS --without-K #-}
module Util.HoTT.Equiv.Induction where

open import Util.HoTT.HLevel.Core
open import Util.HoTT.Equiv
open import Util.HoTT.Univalence.ContrFormulation
open import Util.Prelude

private
variable
α β γ : Level

G-≃ : {A : Set α} (P : Σ[ B  Set α ] (A  B)  Set β)
P (A , ≃-refl)
{B} (A≃B : A  B)
P (B , A≃B)
G-≃ {A = A} P p {B} A≃B = subst P (univalenceProp A (A , ≃-refl) (B , A≃B)) p

abstract
G-≃-β : {A : Set α} (P : Σ[ B  Set α ] (A  B)  Set β)
(p : P (A , ≃-refl))
G-≃ P p ≃-refl  p
G-≃-β {A = A} P p = subst  q  subst P q p  p) (sym go) refl
where
go : univalenceProp A (A , ≃-refl) (A , ≃-refl)  refl
go = IsContr→IsSet (univalenceContr A) _ _

H-≃ : {A : Set α} (P : (B : Set α)  A  B  Set β)
P A ≃-refl
{B} (A≃B : A  B)
P B A≃B
H-≃ P p A≃B = G-≃  { (B , A≃B)  P B A≃B }) p A≃B

abstract
H-≃-β : {A : Set α} (P : (B : Set α)  A  B  Set β)
(p : P A ≃-refl)
H-≃ P p ≃-refl  p
H-≃-β P p = G-≃-β  { (B , A≃B)  P B A≃B }) p

J-≃ : (P : (A B : Set α)  A  B  Set β)
(∀ A  P A A ≃-refl)
{A B} (A≃B : A  B)
P A B A≃B
J-≃ P p {A} {B} A≃B = H-≃  B A≃B  P A B A≃B) (p A) A≃B

abstract
J-≃-β : (P : (A B : Set α)  A  B  Set β)
(p :  A  P A A ≃-refl)
{A}
J-≃ P p ≃-refl  p A
J-≃-β P p {A} = H-≃-β  B A≃B  P A B A≃B) (p A)

H-IsEquiv : {A : Set α} (P : (B : Set α)  (A  B)  Set β)
P A id
{B} (f : A  B)
IsEquiv f
P B f
H-IsEquiv P p f f-equiv
= H-≃  B A≃B  P B (A≃B .forth)) p
(record { forth = f ; isEquiv = f-equiv })

J-IsEquiv : (P : (A B : Set α)  (A  B)  Set β)
(∀ A  P A A id)
{A B} (f : A  B)
IsEquiv f
P A B f
J-IsEquiv P p f f-equiv
= J-≃  A B A≃B  P A B (A≃B .forth)) p
(record { forth = f ; isEquiv = f-equiv })