module Hashimoto where

open import Data.Unit
open import Data.Product
open import Data.Sum
open import Data.Function using (_∘_)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality

_↝_ : Set → Set → Set1
A ↝ B = A → B → Set

simple : ∀ {A B} → (A ↝ B) → Set
simple R = ∀ {a b₁ b₂} →  R a b₁ → R a b₂ → b₁ ≡ b₂ 

entire : ∀ {A B} → (A ↝ B) → Set
entire R = ∀ a → ∃ (λ b → R a b)

injective : ∀ {A B} → (A ↝ B) → Set
injective R = ∀ {a₁ a₂ b} → R a₁ b → R a₂ b → a₁ ≡ a₂

surjective : ∀ {A B} → (A ↝ B) → Set
surjective R = ∀ b → ∃ (λ a → R a b)

_˘ : ∀ {A B} → (A ↝ B) → (B ↝ A)
(R ˘) b a = R a b 

-- axiom of choice 

ac : ∀ {A B} → (R : A ↝ B) →
         (∀ a → ∃ (λ b → R a b)) → ∃ {A → B} (λ f → ∀ a → R a (f a))
ac R R-entire = ((λ a → proj₁ (R-entire a)) , λ a → proj₂ (R-entire a))

-- simple ⇒ uniqueness?

uniq : ∀ {A B} → (R : A ↝ B) → simple R → 
          (f₁ : A → B) → (∀ a → R a (f₁ a)) →
          (f₂ : A → B) → (∀ a → R a (f₂ a)) →
             ∀ a → f₁ a ≡ f₂ a
uniq R R-simple f₁ f₁⊆R f₂ f₂⊆R a = R-simple (f₁⊆R a) (f₂⊆R a)

-- lifting a function to a relation

fun : ∀ {A B} → (A → B) → (A ↝ B)
fun f a b = f a ≡ b

{-

Let f : A → B be injective. Does there exist an f⁻¹ such that f⁻¹ ∘ f = id?
Perhaps not so in intuinistic logic with proof irrelevence.

If f is also (provably) surjective, one can pick some g ⊆ f˘ using the
axiom of choice (which takes the proof of surjectivity of f as an
argument) and further prove that g ∘ f = id using injectivity.

-}

inv-sur : ∀ {A B} → (f : A → B) → injective (fun f) → surjective (fun f) →
             ∃ {B → A} (λ f⁻¹ → (∀ a → f⁻¹ (f a) ≡ a))
inv-sur f f-inj f-sur with ac ((fun f) ˘) f-sur
... | (g , fgb≡b) =  (g , λ a → f-inj {g (f a)} {a} {f a} (fgb≡b (f a)) refl)

{-
What if f is not surjective?

Assume that B is some type with decidable equality.
Let P : B → Set be a predicate and let's pick A = Σ B (λ b → P b).
That is, A is the subset of B for which P holds. Let f be proj₁.
Certainly f is injective. Furthermore, assume that A is non-empty.
-}

postulate B : Set
postulate eqB : (b₁ b₂ : B) → (b₁ ≡ b₂) ⊎ (¬ (b₁ ≡ b₂))

postulate pf-irr : (P : B → Set) → ∀ {b} → (p₁ : P b) → (p₂ : P b) → p₁ ≡ p₂

A : (B → Set) → Set
A P = Σ B (λ b → P b)

f : ∀ {P} → A P → B
f = proj₁

f-inj : ∀ {P} → injective (fun (f {P}))  -- we need proof irrelevence to prove this.
f-inj {P} {(.b , Pb₁)} {(.b , Pb₂)} {b} refl refl = cong (λ p → (b , p)) (pf-irr P Pb₁ Pb₂)

{- Assume that inv-sur holds without the surjectivity constraint.
   Therefore, f has an inverse function f⁻¹ : B → A. 
-}

postulate inv : ∀ {A B} → (f : A → B) → injective (fun f) → 
                   ∃ {B → A} (λ f⁻¹ → (∀ a → f⁻¹ (f a) ≡ a))

{-
Given some b, either

 1. P b holds true. In this case f⁻¹ must map b to (b , p) where p 
    is a proof of P b, since f⁻¹ is the left inverse of f.

 2. P b does not hold. In this case f⁻¹, being a total function,
    still has to map b to something. So let us pick some arbitrary 
    value a₀ = (b₀ , p) in A. Certainly, b₀ does not equal b.

However, that means we now have a decision procedure
(P : B → Set) → ∀ b → (P b ⊎ ¬ (P b)). Just compare the left
component of f⁻¹ b with b. If they equal, we return the proof.
Otherwise, having a proof of P b contradicts the inequality.
-}

em : {P : B → Set} → ∀ b → P b ⊎ ¬ (P b)
em {P} b with inv f (f-inj {P})
...      | (f⁻¹ , f⁻¹fa≡a) with inspect (f⁻¹ b) 
...                        | (b' , Pb') with-≡ _          with eqB b b'
em {P} b | (f⁻¹ , f⁻¹fa≡a) | (b' , Pb') with-≡ _          | inj₁ b≡b'  = inj₁ (subst P (sym b≡b') Pb')
em {P} b | (f⁻¹ , f⁻¹fa≡a) | (b' , Pb') with-≡ b'Pb'≡f⁻¹b | inj₂ ¬b≡b' = 
   inj₂ (λ Pb →
           let f⁻¹b≡bPb : f⁻¹ b ≡ (b , Pb)
               f⁻¹b≡bPb = f⁻¹fa≡a (b , Pb)
               bPb≡b'Pb' : (b , Pb) ≡ (b' , Pb')
               bPb≡b'Pb' = sym (trans b'Pb'≡f⁻¹b f⁻¹b≡bPb)
               b≡b' : b ≡ b'
               b≡b' = cong proj₁ bPb≡b'Pb'
           in ¬b≡b' b≡b')

{-
Having f⁻¹ introduces the law of excluded middle. Therefore
it is perhaps not something we can have in intuinistic logic.
-}

{- Nakano san's question: given injective functions f : A → B and g : B → A,
   is there a bijection A → B? 

nakano : {A B : Set} → (f : A → B) → injective (fun f) → (g : B → A) → injective (fun g) →
           ∃ {A → B} (λ h → injective (fun h) × surjective (fun h))
nakano f f-inj g g-inj = 
    (f ∘ g ∘ f , 
     (λ fgfa₁≡b fgfa₂≡b → {!!}) , 
     λ b → {!!})

-}