OneDist.agda

open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Product 

open ≡-Reasoning

variable 
  A : Set
  B : Set 

record _~_ (A : Set) (B : Set) : Set where
  constructor bij 
  field 
    to   : A -> B 
    from : B -> A 
    from-to : ∀ x -> to (from x) ≡ x 
    to-from : ∀ x -> from (to x) ≡ x 

open _~_

uniq : ⊤ ~ A -> (a : A) -> (a' : A) -> a ≡ a' 
uniq h a a' = 
  begin 
    a
  ≡⟨ sym (from-to h a) ⟩ 
    to h (from h a) 
  ≡⟨ cong (to h) refl ⟩ 
    to h (from h a') 
  ≡⟨ from-to h a' ⟩ 
    a'
  ∎

lemma : ⊤ ~ (A × B) -> ⊤ ~ A 
to (lemma h) = λ a -> proj₁ (to h a)
from (lemma h) = λ _ -> tt
from-to (lemma h) a = 
  let b = proj₂ (to h tt) 
  in cong proj₁ (uniq h (proj₁ (to h tt) , b) (a , b))
to-from (lemma h) tt = refl