michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/hott) adjust funext_from_ua.lea to typeclass axioms

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-20 12:05:45 -05:00 committed by Leonardo de Moura
parent 2d9621892b
commit 1f6b6ff8e6
2 changed files with 11 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/hott/axioms/ua.lean
View file

@ -8,18 +8,18 @@ open path Equiv
--Ensure that the types compared are in the same universe
section
universe variable l
variables (A B : Type.{l})
variables {A B : Type.{l}}
definition isequiv_path (H : A ≈ B) :=
(@IsEquiv.transport Type (λX, X) A B H)
definition equiv_path (H : A ≈ B) : A ≃ B :=
Equiv.mk _ (isequiv_path A B H)
Equiv.mk _ (isequiv_path H)
end
inductive ua_type [class] : Type :=
mk : (Π (A B : Type), IsEquiv (equiv_path A B)) → ua_type
mk : (Π (A B : Type), IsEquiv (@equiv_path A B)) → ua_type
namespace ua_type
@ -28,7 +28,7 @@ namespace ua_type
parameters [F : ua_type.{k}] {A B: Type.{k}}
-- Make the Equivalence given by the axiom an instance
protected definition inst [instance] : IsEquiv (equiv_path.{k} A B) :=
protected definition inst [instance] : IsEquiv (@equiv_path.{k} A B) :=
rec_on F (λ H, H A B)
-- This is the version of univalence axiom we will probably use most often

24
library/hott/funext_from_ua.lean
View file

@ -2,35 +2,25 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
import hott.equiv hott.funext_varieties
import hott.equiv hott.funext_varieties hott.axioms.ua
import data.prod data.sigma data.unit
open path function prod sigma truncation Equiv IsEquiv unit
definition isequiv_path {A B : Type} (H : A ≈ B) :=
(@IsEquiv.transport Type (λX, X) A B H)
definition equiv_path {A B : Type} (H : A ≈ B) : A ≃ B :=
Equiv.mk _ (isequiv_path H)
-- First, define an axiom free variant of Univalence
definition ua_type := Π (A B : Type), IsEquiv (@equiv_path A B)
open path function prod sigma truncation Equiv IsEquiv unit ua_type
context
universe variables l
parameter {ua : ua_type.{l+1}}
parameter [UA : ua_type.{l+1}]
protected theorem ua_isequiv_postcompose {A B : Type.{l+1}} {C : Type}
{w : A → B} {H0 : IsEquiv w} : IsEquiv (@compose C A B w) :=
let w' := Equiv.mk w H0 in
let eqinv : A ≈ B := (equiv_path⁻¹ w') in
let eqinv : A ≈ B := ((@IsEquiv.inv _ _ _ (@ua_type.inst UA A B)) w') in
let eq' := equiv_path eqinv in
IsEquiv.adjointify (@compose C A B w)
(@compose C B A (IsEquiv.inv w))
(λ (x : C → B),
have eqretr : eq' ≈ w',
from (@retr _ _ (@equiv_path A B) (ua A B) w'),
from (@retr _ _ (@equiv_path A B) (@ua_type.inst UA A B) w'),
have invs_eq : (equiv_fun eq')⁻¹ ≈ (equiv_fun w')⁻¹,
from inv_eq eq' w' eqretr,
have eqfin : (equiv_fun eq') ∘ ((equiv_fun eq')⁻¹ ∘ x) ≈ x,
@ -48,7 +38,7 @@ context
)
(λ (x : C → A),
have eqretr : eq' ≈ w',
from (@retr _ _ (@equiv_path A B) (ua A B) w'),
from (@retr _ _ (@equiv_path A B) ua_type.inst w'),
have invs_eq : (equiv_fun eq')⁻¹ ≈ (equiv_fun w')⁻¹,
from inv_eq eq' w' eqretr,
have eqfin : (equiv_fun eq')⁻¹ ∘ ((equiv_fun eq') ∘ x) ≈ x,
@ -124,7 +114,7 @@ context
from (λ x, @equiv_contr_unit(P x) (allcontr x)),
have psim : Π (x : A), P x ≈ U x,
from (λ x, @IsEquiv.inv _ _
(@equiv_path (P x) (U x)) (ua2 (P x) (U x)) (pequiv x)),
equiv_path ua_type.inst (pequiv x)),
have p : P ≈ U,
from @ua_implies_funext_nondep.{l+2 l+1} ua3 A Type.{l+2} P U psim,
have tU' : is_contr (A → unit),