{-# OPTIONS --without-K #-}
module function.extensionality.computation where

open import equality
open import function.isomorphism.core
open import function.core
open import function.extensionality.core
open import function.extensionality.proof
open import function.extensionality.strong

funext-inv-hom : ∀ {i j}{X : Set i}{Y : X → Set j}
               → {f₁ f₂ f₃ : (x : X) → Y x}
               → (p₁ : f₁ ≡ f₂)
               → (p₂ : f₂ ≡ f₃)
               → funext-inv (p₁ · p₂)
               ≡ (λ x → funext-inv p₁ x · funext-inv p₂ x)
funext-inv-hom refl p₂ = refl

funext-hom : ∀ {i j}{X : Set i}{Y : X → Set j}
           → {f₁ f₂ f₃ : (x : X) → Y x}
           → (h₁ : (x : X) → f₁ x ≡ f₂ x)
           → (h₂ : (x : X) → f₂ x ≡ f₃ x)
           → funext (λ x → h₁ x · h₂ x)
           ≡ funext h₁ · funext h₂
funext-hom h₁ h₂ = begin
    funext (λ x → h₁ x · h₂ x)
  ≡⟨ sym (ap funext (ap₂ (λ u v x → u x · v x)
                         (_≅_.iso₁ strong-funext-iso h₁)
                         (_≅_.iso₁ strong-funext-iso h₂))) ⟩
    funext (λ x → funext-inv (funext h₁) x · funext-inv (funext h₂) x)
  ≡⟨ sym (ap funext (funext-inv-hom (funext h₁) (funext h₂))) ⟩
    funext (funext-inv (funext h₁ · funext h₂))
  ≡⟨ _≅_.iso₂ strong-funext-iso (funext h₁ · funext h₂) ⟩
    funext h₁ · funext h₂
  ∎
  where open ≡-Reasoning

funext-inv-ap : ∀ {i j k}{X : Set i}{Y : X → Set j}{Z : X → Set k}
              → (g : {x : X} → Y x → Z x)
              → {f₁ f₂ : (x : X) → Y x}
              → (p : f₁ ≡ f₂)
              → funext-inv (ap (_∘'_ g) p)
              ≡ ((λ x → ap g (funext-inv p x)))
funext-inv-ap g refl = refl

funext-ap : ∀ {i j k}{X : Set i}{Y : X → Set j}{Z : X → Set k}
          → (g : {x : X} → Y x → Z x)
          → {f₁ f₂ : (x : X) → Y x}
          → (h : (x : X) → f₁ x ≡ f₂ x)
          → funext (λ x → ap g (h x))
          ≡ ap (_∘'_ g) (funext h)
funext-ap g h = begin
    funext (λ x → ap g (h x))
  ≡⟨ sym (ap funext (ap (λ h x → ap g (h x))
                    (_≅_.iso₁ strong-funext-iso h))) ⟩
    funext (λ x → ap g (funext-inv (funext h) x))
  ≡⟨ ap funext (sym (funext-inv-ap g (funext h))) ⟩
    funext (funext-inv (ap (_∘'_ g) (funext h)))
  ≡⟨ _≅_.iso₂ strong-funext-iso _ ⟩
    ap (_∘'_ g) (funext h)
  ∎
  where open ≡-Reasoning