hedberg.agda

{-# OPTIONS --without-K #-}
open import Data.Empty
open import Data.Sum
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

_∙_ = trans

∙-unitʳ : ∀ {A : Set} {x y : A} (p : x ≡ y) → p ∙ refl ≡ p
∙-unitʳ refl = refl

transport : ∀ {A : Set} (P : A → Set) {x y} → x ≡ y → P x → P y
transport P refl = id



apd : ∀ {A : Set} {P : A → Set} (f : (x : A) → P x)
  → ∀ {x y} (p : x ≡ y) → transport P p (f x) ≡ f y
apd f refl = refl

happly : ∀ {A : Set} {P : A → Set} {f g : (x : A) → P x}
  → f ≡ g
  → ∀ x → f x ≡ g x
happly refl x = refl

lemma-296 : ∀ {X : Set} {A B : X → Set} {x y : X}
  → (p : x ≡ y)
  → {f : A x → B x}
  → {g : A y → B y}
  →               transport (λ x → A x → B x) p  f    ≡ g
  → ∀ (a : A x) → transport (λ x → B x) p (f a) ≡ g (transport (λ x → A x) p a)
lemma-296 refl f≡g = happly f≡g

axiom-k : Set → Set
axiom-k A = ∀ (x : A) (p : x ≡ x) → p ≡ refl

is-prop : Set → Set
is-prop A = ∀ (x y : A) → x ≡ y

is-set : Set → Set
is-set A = ∀ (x y : A) (p q : x ≡ y) → p ≡ q

postulate
  funext : ∀ {A B : Set} {f g : A → B}
    → (∀ x → f x ≡ g x)
    → f ≡ g

¬-is-prop : ∀ {A : Set} → is-prop (¬ A)
¬-is-prop f g = funext λ x → ⊥-elim (f x)

theorem-721 : ∀ {A : Set} → axiom-k A → is-set A
theorem-721 f x .x p refl = f x p

cancelˡ : ∀ {A : Set} {x y z : A} {p : x ≡ y} {r s : y ≡ z}
  → p ∙ r ≡ p ∙ s
  → r ≡ s
cancelˡ {p = refl} = id

lemma-2112 : ∀ {A : Set} {a x₁ x₂ : A} {p : x₁ ≡ x₂} {q : a ≡ x₁}
  → transport (λ x → a ≡ x) p q ≡ q ∙ p
lemma-2112 {p = refl} = sym (∙-unitʳ _)

theorem-722 : ∀ {A : Set}
  → ((x y : A) → ¬ ¬ x ≡ y → x ≡ y)
  → (x : A) (p : x ≡ x) → p ≡ refl
theorem-722 {A} f x p =
  let ρ : (x : A) → ¬ ¬ x ≡ x
      ρ x = λ ¬x≡x → ⊥-elim (¬x≡x refl)
  in cancelˡ (begin
  f x x (ρ x) ∙ p ≡⟨ sym (lemma-2112 {p = p}) ⟩
  transport (x ≡_) p (f x x (ρ x)) ≡⟨ lemma-296 p (apd (f x) p) (ρ x) ⟩
  f x x (transport (λ z → ¬ ¬ x ≡ z) p (ρ x)) ≡⟨ cong (f x x) (¬-is-prop _ _) ⟩
  f x x (ρ x) ≡⟨ sym (∙-unitʳ _) ⟩
  f x x (ρ x) ∙ refl ∎)
  where open import Relation.Binary.Reasoning.Setoid (setoid _)