Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: HoTT_coq_090.v Sprache: Coq

Original von: Coq^©

Require Import TestSuite.admit.
(** I'm not sure if this tests what I want it to test... *)
Set Implicit Arguments.
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.
Arguments paths_rec [A] a P f y p.
Arguments paths_rect [A] a P f y p.

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. *)
Definition inverse {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. *)
Arguments inverse {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.

Instance isequiv_path {A B : Type} (p : A = B)
  : IsEquiv (transport (fun X:Type => X) p) | 0.
Proof.
  unshelve refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
  admit.
Defined.

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
    | exact match 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 ].

  - pose proof (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 *)".
*)

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.