f513538631
remove funext class, remove a couple of sorry's, add characterization of equality in trunctypes, use Jeremy's format for headers everywhere in the HoTT library, continue working on Yoneda embedding
47 lines
1.5 KiB
Text
47 lines
1.5 KiB
Text
/-
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
|
|
Hedberg's Theorem: every type with decidable equality is a hset
|
|
-/
|
|
|
|
prelude
|
|
import init.trunc
|
|
open eq eq.ops nat is_trunc sigma
|
|
|
|
-- TODO(Leo): move const coll and path_coll to a different file?
|
|
private definition const {A B : Type} (f : A → B) := ∀ x y, f x = f y
|
|
private definition coll (A : Type) := Σ f : A → A, const f
|
|
private definition path_coll (A : Type) := ∀ x y : A, coll (x = y)
|
|
|
|
context
|
|
parameter {A : Type}
|
|
hypothesis [h : decidable_eq A]
|
|
variables {x y : A}
|
|
|
|
private definition pc [reducible] : path_coll A :=
|
|
λ a b, decidable.rec_on (h a b)
|
|
(λ p : a = b, ⟨(λ q, p), λ q r, rfl⟩)
|
|
(λ np : ¬ a = b, ⟨(λ q, q), λ q r, absurd q np⟩)
|
|
|
|
private definition f [reducible] : x = y → x = y :=
|
|
sigma.rec_on (pc x y) (λ f c, f)
|
|
|
|
private definition f_const (p q : x = y) : f p = f q :=
|
|
sigma.rec_on (pc x y) (λ f c, c p q)
|
|
|
|
private definition aux (p : x = y) : p = (f (refl x))⁻¹ ⬝ (f p) :=
|
|
have aux : refl x = (f (refl x))⁻¹ ⬝ (f (refl x)), from
|
|
eq.rec_on (f (refl x)) rfl,
|
|
eq.rec_on p aux
|
|
|
|
definition is_hset_of_decidable_eq : is_hset A :=
|
|
is_hset.mk A (λ x y p q, calc
|
|
p = (f (refl x))⁻¹ ⬝ (f p) : aux
|
|
... = (f (refl x))⁻¹ ⬝ (f q) : f_const
|
|
... = q : aux)
|
|
end
|
|
|
|
attribute is_hset_of_decidable_eq [instance]
|