-- 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 })