Quelle HoTT_coq_091.v Sprache: Coq

Set Implicit Arguments.

Set Printing Universes.

Set Asymmetric Patterns.

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 transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
  match p with idpath => u end.

Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
  := match p with idpath => idpath end.
Arguments ap {A B} f {x y} p : simpl nomatch.

Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
  forall x : A, r (s x) = x.

(** 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 {_} _.

Inductive type_eq (A : Type) : Type -> Type :=
| type_eq_refl : type_eq A A
| type_eq_impossible : False -> forall B : Type, type_eq A B.

Definition type_eq_sym {A B} (p : type_eq A B) : type_eq B A
  := match p in (type_eq _ B) return (type_eq B A) with
       | type_eq_refl => type_eq_refl _
       | type_eq_impossible f B => type_eq_impossible _ f A
     end.

Definition type_eq_sym_type_eq_sym {A B} (p : type_eq A B) : type_eq_sym (type_eq_sym p) = p
  := match p as p return type_eq_sym (type_eq_sym p) = p with
       | type_eq_refl => idpath
       | type_eq_impossible f _ => idpath
     end.

Module Type LiftT.
  Section local.
    Let type_cast_up_type : Type.
    Proof.
      let U0 := constr:(Type) in
      let U1 := constr:(Type) in
      let unif := constr:(U0 : U1) in
      exact (forall T : U0, { T' : U1 & type_eq T' T }).
    Defined.

    Axiom type_cast_up : type_cast_up_type.
  End local.

  Definition Lift (T : Type) := projT1 (type_cast_up T).
  Definition lift {T} : T -> Lift T
    := match projT2 (type_cast_up T) in (type_eq _ T') return T' -> Lift T with
         | type_eq_refl => fun x => x
         | type_eq_impossible bad _ => match bad with end
       end.
  Section equiv.
    Definition lower' {T} : Lift T -> T
      := match projT2 (type_cast_up T) in (type_eq _ T') return Lift T -> T' with
           | type_eq_refl => fun x => x
           | type_eq_impossible bad _ => match bad with end
         end.
    Definition lift_lower {T} (x : Lift T) : lift (lower' x) = x.
    Proof.
      unfold lower', lift.
      destruct (projT2 (type_cast_up T)) as [|[]].
      reflexivity.
    Defined.
    Definition lower_lift {T} (x : T) : lower' (lift x) = x.
    Proof.
      unfold lower', lift, Lift in *.
      destruct (type_cast_up T) as [T' p]; simpl.
      let y := match goal with |- ?y => constr:(y) end in
      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
      generalize (type_eq_sym p); intro p'; clear p.
      destruct p' as [|[]]; simpl.
      reflexivity.
    Defined.

    Global Instance isequiv_lift A : IsEquiv (@lift A).
    Proof.
      refine (@BuildIsEquiv
                _ _
                lift lower'
                lift_lower
                lower_lift
                _).
      compute.
      intro x.
      destruct (type_cast_up A) as [T' p].
      let y := match goal with |- ?y => constr:(y) end in
      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
      generalize (type_eq_sym p); intro p'; clear p.
      destruct p' as [|[]]; simpl.
      reflexivity.
    Defined.
  End equiv.
  Definition lower {A} := (@equiv_inv _ _ (@lift A) _).
End LiftT.

Module Lift : LiftT.
  Section local.
    Let type_cast_up_type : Type.
    Proof.
      let U0 := constr:(Type) in
      let U1 := constr:(Type) in
      let unif := constr:(U0 : U1) in
      exact (forall T : U0, { T' : U1 & type_eq T' T }).
    Defined.

    Definition type_cast_up : type_cast_up_type
      := fun T => existT (fun T' => type_eq T' T) T (type_eq_refl _).
  End local.

  Definition Lift (T : Type) := projT1 (type_cast_up T).
  Definition lift {T} : T -> Lift T
    := match projT2 (type_cast_up T) in (type_eq _ T') return T' -> Lift T with
         | type_eq_refl => fun x => x
         | type_eq_impossible bad _ => match bad with end
       end.
  Section equiv.
    Definition lower' {T} : Lift T -> T
      := match projT2 (type_cast_up T) in (type_eq _ T') return Lift T -> T' with
           | type_eq_refl => fun x => x
           | type_eq_impossible bad _ => match bad with end
         end.
    Definition lift_lower {T} (x : Lift T) : lift (lower' x) = x.
    Proof.
      unfold lower', lift.
      destruct (projT2 (type_cast_up T)) as [|[]].
      reflexivity.
    Defined.
    Definition lower_lift {T} (x : T) : lower' (lift x) = x.
    Proof.
      unfold lower', lift, Lift in *.
      destruct (type_cast_up T) as [T' p]; simpl.
      let y := match goal with |- ?y => constr:(y) end in
      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
      generalize (type_eq_sym p); intro p'; clear p.
      destruct p' as [|[]]; simpl.
      reflexivity.
    Defined.

    Global Instance isequiv_lift A : IsEquiv (@lift A).
    Proof.
      refine (@BuildIsEquiv
                _ _
                lift lower'
                lift_lower
                lower_lift
                _).
      compute.
      intro x.
      destruct (type_cast_up A) as [T' p].
      let y := match goal with |- ?y => constr:(y) end in
      let P := match (eval pattern p in y) with ?f p => constr:(f) end in
      apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *.
      generalize (type_eq_sym p); intro p'; clear p.
      destruct p' as [|[]]; simpl.
      reflexivity.
    Defined.
  End equiv.
  Definition lower {A} := (@equiv_inv _ _ (@lift A) _).
End Lift.
(* Toplevel input, characters 15-24:
Anomaly: Invalid argument: enforce_eq_instances called with instances of different lengths.
Please report. *)

quality98%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.