Library HoTT.Universes.UniverseLevel
Universe Levels
Definition Lift@{i j | i < j} (A : Type@{i}) : Type@{j}
:= A.
Definition lift {A} : A → Lift A := fun x ⇒ x.
Definition lower {A} : Lift A → A := fun x ⇒ x.
Definition lift2 {A B} (f : ∀ x : A, B x) : ∀ x : Lift A, Lift (B (lower x))
:= f.
Definition lower2 {A B} (f : ∀ x : Lift A, Lift (B (lower x))) : ∀ x : A, B x
:= f.
:= A.
Definition lift {A} : A → Lift A := fun x ⇒ x.
Definition lower {A} : Lift A → A := fun x ⇒ x.
Definition lift2 {A B} (f : ∀ x : A, B x) : ∀ x : Lift A, Lift (B (lower x))
:= f.
Definition lower2 {A B} (f : ∀ x : Lift A, Lift (B (lower x))) : ∀ x : A, B x
:= f.
We make lift and lower opaque so that typeclass resolution doesn't pick up isequiv_lift as an instance of IsEquiv idmap and wreak havoc.
#[global] Typeclasses Opaque lift lower lift2 lower2.
Instance isequiv_lift T : IsEquiv (@lift T)
:= @Build_IsEquiv
_ _
(@lift T)
(@lower T)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath).
Instance isequiv_lift2 A B : IsEquiv (@lift2 A B)
:= @Build_IsEquiv
_ _
(@lift2 A B)
(@lower2 A B)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath).
Instance lift_isequiv {A B} (f : A → B) {H : IsEquiv f} : @IsEquiv (Lift A) (Lift B) (lift2 f)
:= @Build_IsEquiv
(Lift A) (Lift B)
(lift2 f)
(lift2 (f^-1))
(fun x ⇒ ap lift (eisretr f (lower x)))
(fun x ⇒ ap lift (eissect f (lower x)))
(fun x ⇒ ((ap (ap lift) (eisadj f (lower x)))
@ (ap_compose f lift _)^)
@ (@ap_compose A (Lift A) (Lift B) lift (lift2 f) _ _ _)).
Instance lower_isequiv {A B} (f : Lift A → Lift B) {H : IsEquiv f} : @IsEquiv A B (lower2 f)
:= @Build_IsEquiv
_ _
(lower2 f)
(lower2 (f^-1))
(fun x ⇒ ap lower (eisretr f (lift x)))
(fun x ⇒ ap lower (eissect f (lift x)))
(fun x ⇒ ((ap (ap lower) (eisadj f (lift x)))
@ (ap_compose f lower _)^)
@ (@ap_compose (Lift A) A B lower (lower2 f) _ _ _)).
Definition lower_equiv {A B} (e : Equiv (Lift A) (Lift B)) : Equiv A B
:= @Build_Equiv A B (lower2 e) _.
Instance isequiv_lift T : IsEquiv (@lift T)
:= @Build_IsEquiv
_ _
(@lift T)
(@lower T)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath).
Instance isequiv_lift2 A B : IsEquiv (@lift2 A B)
:= @Build_IsEquiv
_ _
(@lift2 A B)
(@lower2 A B)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath).
Instance lift_isequiv {A B} (f : A → B) {H : IsEquiv f} : @IsEquiv (Lift A) (Lift B) (lift2 f)
:= @Build_IsEquiv
(Lift A) (Lift B)
(lift2 f)
(lift2 (f^-1))
(fun x ⇒ ap lift (eisretr f (lower x)))
(fun x ⇒ ap lift (eissect f (lower x)))
(fun x ⇒ ((ap (ap lift) (eisadj f (lower x)))
@ (ap_compose f lift _)^)
@ (@ap_compose A (Lift A) (Lift B) lift (lift2 f) _ _ _)).
Instance lower_isequiv {A B} (f : Lift A → Lift B) {H : IsEquiv f} : @IsEquiv A B (lower2 f)
:= @Build_IsEquiv
_ _
(lower2 f)
(lower2 (f^-1))
(fun x ⇒ ap lower (eisretr f (lift x)))
(fun x ⇒ ap lower (eissect f (lift x)))
(fun x ⇒ ((ap (ap lower) (eisadj f (lift x)))
@ (ap_compose f lower _)^)
@ (@ap_compose (Lift A) A B lower (lower2 f) _ _ _)).
Definition lower_equiv {A B} (e : Equiv (Lift A) (Lift B)) : Equiv A B
:= @Build_Equiv A B (lower2 e) _.
This version doesn't force strict containment, i.e. it allows the two universes to possibly be the same.
However, if we don't give the universes as explicit arguments here, then Coq collapses them.
Definition lift'@{i j} {A : Type@{i}} : A → Lift'@{i j} A := fun x ⇒ x.
Definition lower'@{i j} {A : Type@{i}} : Lift'@{i j} A → A := fun x ⇒ x.
Definition lift'2@{i i' j j'} {A : Type@{i}} {B : A → Type@{i'}} (f : ∀ x : A, B x)
: ∀ x : Lift'@{i j} A, Lift'@{i' j'} (B (lower' x))
:= f.
Definition lower'2@{i i' j j'} {A : Type@{i}} {B : A → Type@{i'}}
(f : ∀ x : Lift'@{i j} A, Lift'@{i' j'} (B (lower' x)))
: ∀ x : A, B x
:= f.
Definition lower'@{i j} {A : Type@{i}} : Lift'@{i j} A → A := fun x ⇒ x.
Definition lift'2@{i i' j j'} {A : Type@{i}} {B : A → Type@{i'}} (f : ∀ x : A, B x)
: ∀ x : Lift'@{i j} A, Lift'@{i' j'} (B (lower' x))
:= f.
Definition lower'2@{i i' j j'} {A : Type@{i}} {B : A → Type@{i'}}
(f : ∀ x : Lift'@{i j} A, Lift'@{i' j'} (B (lower' x)))
: ∀ x : A, B x
:= f.
We make lift and lower opaque so that typeclass resolution doesn't pick up isequiv_lift as an instance of IsEquiv idmap and wreak havoc.
#[global] Typeclasses Opaque lift' lower' lift'2 lower'2.
Instance isequiv_lift'@{i j} (T : Type@{i})
: IsEquiv (@lift'@{i j} T)
:= @Build_IsEquiv
_ _
(@lift' T)
(@lower' T)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath).
Instance isequiv_lift'2@{e0 e1 i i' j j'} (A : Type@{i}) (B : A → Type@{j})
: IsEquiv@{e0 e1} (@lift'2@{i i' j j'} A B)
:= @Build_IsEquiv
_ _
(@lift'2 A B)
(@lower'2 A B)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath).
Instance lift'_isequiv@{a b i j i' j'} {A : Type@{a}} {B : Type@{b}}
(f : A → B) {H : IsEquiv f}
: @IsEquiv (Lift'@{i j} A) (Lift'@{i' j'} B) (lift'2 f)
:= @Build_IsEquiv
(Lift' A) (Lift' B)
(lift'2 f)
(lift'2 (f^-1))
(fun x ⇒ ap lift' (eisretr f (lower' x)))
(fun x ⇒ ap lift' (eissect f (lower' x)))
(fun x ⇒ ((ap (ap lift') (eisadj f (lower' x)))
@ (ap_compose f lift' _)^)
@ (@ap_compose A (Lift' A) (Lift' B) lift' (lift'2 f) _ _ _)).
Instance lower'_isequiv@{i j i' j'} {A : Type@{i}} {B : Type@{j}}
(f : Lift'@{i j} A → Lift'@{i' j'} B) {H : IsEquiv f}
: @IsEquiv A B (lower'2 f)
:= @Build_IsEquiv
_ _
(lower'2 f)
(lower'2 (f^-1))
(fun x ⇒ ap lower' (eisretr f (lift' x)))
(fun x ⇒ ap lower' (eissect f (lift' x)))
(fun x ⇒ ((ap (ap lower') (eisadj f (lift' x)))
@ (ap_compose f lower' _)^)
@ (@ap_compose (Lift' A) A B lower' (lower'2 f) _ _ _)).
Definition lower'_equiv@{i j i' j'} {A : Type@{i}} {B : Type@{j}}
(e : Equiv (Lift'@{i j} A) (Lift'@{i' j'} B))
: Equiv A B
:= @Build_Equiv A B (lower'2 e) _.
Instance isequiv_lift'@{i j} (T : Type@{i})
: IsEquiv (@lift'@{i j} T)
:= @Build_IsEquiv
_ _
(@lift' T)
(@lower' T)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath).
Instance isequiv_lift'2@{e0 e1 i i' j j'} (A : Type@{i}) (B : A → Type@{j})
: IsEquiv@{e0 e1} (@lift'2@{i i' j j'} A B)
:= @Build_IsEquiv
_ _
(@lift'2 A B)
(@lower'2 A B)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath)
(fun _ ⇒ idpath).
Instance lift'_isequiv@{a b i j i' j'} {A : Type@{a}} {B : Type@{b}}
(f : A → B) {H : IsEquiv f}
: @IsEquiv (Lift'@{i j} A) (Lift'@{i' j'} B) (lift'2 f)
:= @Build_IsEquiv
(Lift' A) (Lift' B)
(lift'2 f)
(lift'2 (f^-1))
(fun x ⇒ ap lift' (eisretr f (lower' x)))
(fun x ⇒ ap lift' (eissect f (lower' x)))
(fun x ⇒ ((ap (ap lift') (eisadj f (lower' x)))
@ (ap_compose f lift' _)^)
@ (@ap_compose A (Lift' A) (Lift' B) lift' (lift'2 f) _ _ _)).
Instance lower'_isequiv@{i j i' j'} {A : Type@{i}} {B : Type@{j}}
(f : Lift'@{i j} A → Lift'@{i' j'} B) {H : IsEquiv f}
: @IsEquiv A B (lower'2 f)
:= @Build_IsEquiv
_ _
(lower'2 f)
(lower'2 (f^-1))
(fun x ⇒ ap lower' (eisretr f (lift' x)))
(fun x ⇒ ap lower' (eissect f (lift' x)))
(fun x ⇒ ((ap (ap lower') (eisadj f (lift' x)))
@ (ap_compose f lower' _)^)
@ (@ap_compose (Lift' A) A B lower' (lower'2 f) _ _ _)).
Definition lower'_equiv@{i j i' j'} {A : Type@{i}} {B : Type@{j}}
(e : Equiv (Lift'@{i j} A) (Lift'@{i' j'} B))
: Equiv A B
:= @Build_Equiv A B (lower'2 e) _.