RequireImport TestSuite.admit. (** I'm not sure if this tests what I want it to test... *) SetImplicitArguments. Set Universe Polymorphism.
Notation idmap := (fun x => x).
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Arguments idpath {A a} , [A] a.
Arguments paths_ind [A] a P f y p : rename. Arguments paths_rec [A] a P f y p : rename. Arguments paths_rect [A] a P f y p : rename.
Notation"x = y :> A" := (@paths A x y) : type_scope. Notation"x = y" := (x = y :>_) : type_scope.
Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with idpath => idpath end.
(** A typeclass that includes the data making [f] into an adjoint equivalence. *) Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
equiv_inv : B -> A ;
eisretr : Sect equiv_inv f;
eissect : Sect f equiv_inv;
eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.
Arguments eisretr {A B} f {_} _. Arguments eissect {A B} f {_} _. Arguments eisadj {A B} f {_} _.
Record Equiv A B := BuildEquiv {
equiv_fun :> A -> B ;
equiv_isequiv :> IsEquiv equiv_fun
}.
Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end.
(** See above for the meaning of [simpl nomatch]. *) Arguments concat {A x y z} p q : simpl nomatch.
(** The inverse of a path. *) Definitioninverse {A : Type} {x y : A} (p : x = y) : y = x
:= match p with idpath => idpath end.
(** Declaring this as [simpl nomatch] prevents the tactic [simpl] from expanding it out into [match] statements. We only want [inverse] to simplify when applied to an identity path. *) Argumentsinverse {A x y} p : simpl nomatch.
(** Note that you can use the built-in Coq tactics [reflexivity] and [transitivity] when working with paths, but not [symmetry], because it is too smart for its own good. Instead, you can write [apply symmetry] or [eapply symmetry]. *)
(** The identity path. *) Notation"1" := idpath : path_scope.
(** The composition of two paths. *) Notation"p @ q" := (concat p q) (at level 20) : path_scope.
(** The inverse of a path. *) Notation"p ^" := (inverse p) (at level 3) : path_scope.
(** An alternative notation which puts each path on its own line. Useful as a temporary device during proofs of equalities between very long composites; to turn it on inside a section, say [Open Scope long_path_scope]. *) Notation"p @' q" := (concat p q) (at level 21, left associativity,
format "'[v' p '/' '@'' q ']'") : long_path_scope.
(** An important instance of [paths_rect] is that given any dependent type, one can _transport_ elements of instances of the type along equalities in the base.
[transport P p u] transports [u : P x] to [P y] along [p : x = y]. *) Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
(** See above for the meaning of [simpl nomatch]. *) Arguments transport {A} P {x y} p%_path_scope u : simpl nomatch.
Definition equiv_path (A B : Type) (p : A = B) : Equiv A B
:= @BuildEquiv _ _ (transport (fun X:Type => X) p) _.
Arguments equiv_path : clear implicits.
Definition equiv_adjointify A B (f : A -> B) (g : B -> A) (r : Sect g f) (s : Sect f g) : Equiv A B. Proof.
refine (@BuildEquiv A B f (@BuildIsEquiv A B f g r s _)).
admit. Defined.
Set Printing Universes.
Definition lift_id_type : Type. Proof. let U0 := constr:(Type) in let U1 := constr:(Type) in let unif := constr:(U0 : U1) in exact (forall (A : Type) (B : Type), @paths U0 A B -> @paths U1 A B). Defined.
Definition lower_id_type : Type. Proof. let U0 := constr:(Type) in let U1 := constr:(Type) in let unif := constr:(U0 : U1) in exact ((forall (A : Type) (B : Type), IsEquiv (equiv_path (A : U0) (B : U0)))
-> forall (A : Type) (B : Type), @paths U1 A B -> @paths U0 A B). Defined.
Definition lift_id : lift_id_type := fun A B p => match p in @paths _ _ B return @paths Type (A : Type) (B : Type) with
| idpath => idpath end.
Definition lower_id : lower_id_type. Proof. intros ua A B p.
specialize (ua A B). apply (@equiv_inv _ _ (equiv_path A B) _). simpl. pose (f := transport idmap p : A -> B). pose (g := transport idmap p^ : B -> A).
refine (@equiv_adjointify
_ _
f g
_ _);
subst f g; unfold transport, inverse;
clear ua;
[ intro x
| exactmatch p as p in (_ = B) return
(forall x : (A : Type),
@paths (* Top.904 *)
A match match
p in (paths _ a) return (@paths (* Top.906 *) Type (* Top.900 *) a A) with
| idpath => @idpath (* Top.906 *) Type (* Top.900 *) A end in (paths _ a) return a with
| idpath => match p in (paths _ a) return a with
| idpath => x end end x) with
| idpath => fun _ => idpath end ].
- poseproof (match p as p in (_ = B) return
(forall x : (B : Type), match p in (_ = a) return (a : Type) with
| idpath => match match p in (_ = a) return (@paths Type (a : Type) (A : Type)) with
| idpath => idpath end in (_ = a) return (a : Type) with
| idpath => x end end = x) with
| idpath => fun _ => idpath end x) as p'.
admit. Defined. (* Error: Illegal application:
The term "paths (* Top.96 *) "forall A : Type (* Top.96 *), A -> A -> Type (* Top.96 *)"
cannot be applied to the terms "Type (* Top.100 *)" : "Type (* Top.100+1 *)" "a" : "Type (* Top.60 *)" "A" : "Type (* Top.57 *)"
The 2nd term has type"Type (* Top.60 *)" which should be coercible to "Type (* Top.100 *)".
*)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
