Incompatibility.agda

{-# OPTIONS --without-K #-}
module Incompatibility where

open import Data.Bool
open import Data.Empty
open import Data.Product
open import Data.Unit
open import Function
open import Level
open import Relation.Binary.PropositionalEquality

infixr 4 _≃_

record _≃_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor equiv
  field
    to   : A → B
    from : B → A
    α : ∀ x → to (from x) ≡ x
    β : ∀ y → from (to y) ≡ y

id-to-equiv : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A ≃ B
id-to-equiv refl = equiv
  id id (λ _ → refl) (λ _ → refl)

postulate
  -- (Part of) the univalence axiom.
  equiv-to-id : ∀ {ℓ} {A B : Set ℓ} → (A ≃ B) → (A ≡ B)
  
  -- Function extensionality (note that it follows from the univalence
  -- axiom, but for simplicity I just assume it).
  ext : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
    (∀ x → f x ≡ g x) → f ≡ g

eq : (⊤ → Bool × Bool) ≡ (Bool → Bool)
eq = equiv-to-id $ equiv
  (λ f b → if b then proj₁ (f _) else proj₂ (f _))
  (λ f _ → f true , f false)
  (λ f → ext λ {true → refl; false → refl})
  (λ f → ext λ _ → refl)

module _ (domain : ∀ {ℓ} {A B C D : Set ℓ} →
  (A → B) ≡ (C → D) → A ≡ C) where

  open ≡-Reasoning
  open _≃_ (id-to-equiv (domain eq))

  bad : true ≡ false
  bad = begin
    true            ≡⟨ sym (α true) ⟩
    to (from true)  ≡⟨⟩
    to tt           ≡⟨⟩
    to (from false) ≡⟨ α false ⟩
    false           ∎