2014-08-11 17:35:25 -07:00
|
|
|
|
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
|
|
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
2014-10-22 22:24:31 -07:00
|
|
|
|
-- Author: Jeremy Avigad, Jakob von Raumer
|
2014-08-11 17:35:25 -07:00
|
|
|
|
-- Ported from Coq HoTT
|
|
|
|
|
|
|
|
|
|
-- TODO: take a look at the Coq tricks
|
2014-11-06 13:34:57 -05:00
|
|
|
|
import hott.path hott.equiv
|
2014-09-09 13:20:04 -07:00
|
|
|
|
open path
|
2014-08-11 17:35:25 -07:00
|
|
|
|
|
|
|
|
|
-- Funext
|
|
|
|
|
-- ------
|
|
|
|
|
|
2014-11-06 19:41:08 -05:00
|
|
|
|
axiom funext {A : Type} {P : A → Type} (f g : Πx, P x) : IsEquiv (@apD10 A P f g)
|
2014-08-11 17:35:25 -07:00
|
|
|
|
|
2014-11-06 19:41:08 -05:00
|
|
|
|
theorem funext_instance [instance] {A : Type} {P : A → Type} (f g : Πx, P x) :
|
2014-11-04 09:49:07 -05:00
|
|
|
|
IsEquiv (@apD10 A P f g) :=
|
|
|
|
|
@funext A P f g
|
|
|
|
|
|
2014-11-06 19:41:08 -05:00
|
|
|
|
definition path_forall {A : Type} {P : A → Type} (f g : Πx, P x) : f ∼ g → f ≈ g :=
|
2014-11-04 09:49:07 -05:00
|
|
|
|
IsEquiv.inv !apD10
|
2014-08-11 17:35:25 -07:00
|
|
|
|
|
2014-11-06 19:41:08 -05:00
|
|
|
|
definition path_forall2 {A B : Type} {P : A → B → Type} (f g : Πx y, P x y) :
|
|
|
|
|
(Πx y, f x y ≈ g x y) → f ≈ g :=
|
|
|
|
|
λE, path_forall f g (λx, path_forall (f x) (g x) (E x))
|