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 → {!!}) -}