Quelle HoTT_coq_108.v Sprache: Coq

Require Import TestSuite.admit.
(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
(* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *)
(* File reduced by coq-bug-finder from 139 lines to 124 lines. *)
Set Universe Polymorphism.
Reserved Notation "g 'o' f" (at level 40, left associativity).
Generalizable All Variables.
Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Arguments idpath {A a} , [A] a.
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.

Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
: forall x, f x = g x
  := fun x => match h with idpath => idpath end.

Definition ap11 {A B} {f g:A->B} (h:f=g) {x y:A} (p:x=y) : f x = g y.
  admit.
Defined.
Class IsEquiv {A B : Type} (f : A -> B) := {}.
Class Contr_internal (A : Type) := BuildContr {
                                       center : A ;
                                       contr : (forall y : A, center = y)
                                     }.

Arguments center A {_}.

Inductive trunc_index : Type :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.

Fixpoint nat_to_trunc_index (n : nat) : trunc_index
  := match n with
       | 0 => trunc_S (trunc_S minus_two)
       | S n' => trunc_S (nat_to_trunc_index n')
     end.

Coercion nat_to_trunc_index : nat >-> trunc_index.

Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
  match n with
    | minus_two => Contr_internal A
    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
  end.
Class IsTrunc (n : trunc_index) (A : Type) : Type :=
  Trunc_is_trunc : IsTrunc_internal n A.

#[export] Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)
: IsTrunc n (x = y)
  := H x y.

Notation Contr := (IsTrunc minus_two).

Notation IsHSet := (IsTrunc 0).

Class Funext :=
  { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
Global Instance contr_forall `{Funext} `{P : A -> Type} `{forall a, Contr (P a)}
: Contr (forall a, P a) | 100.
admit.
Defined.
#[export] Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
: IsTrunc n (forall a, P a) | 100.
Proof.
  generalize dependent P.
  induction n as [ | n' IH]; [ | admit ]; simpl; intros P ?.
                                                        exact _.
Defined.
Set Implicit Arguments.

Record PreCategory :=
  { object :> Type;
    morphism : object -> object -> Type;
    identity : forall x, morphism x x;
    compose : forall s d d', morphism d d' -> morphism s d -> morphism s d';
    trunc_morphism : forall s d, IsHSet (morphism s d) }.

#[export] Existing Instance trunc_morphism.
Infix "o" := (@compose _ _ _ _) : morphism_scope.
Local Open Scope morphism_scope.

Record Functor (C D : PreCategory) :=
  { object_of :> C -> D;
    morphism_of : forall s d, morphism C s d
                              -> morphism D (object_of s) (object_of d);
    composition_of : forall s d d'
                            (m1 : morphism C s d) (m2: morphism C d d'),
                       morphism_of _ _ (m2 o m1)
                       = (morphism_of _ _ m2) o (morphism_of _ _ m1);
    identity_of : forall x, morphism_of _ _ (@identity _ x)
                            = @identity _ (object_of x) }.

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

Section path_functor.
  Context `{Funext}.
  Variable C : PreCategory.
  Variable D : PreCategory.
  Local Notation path_functor'_T F G
    := { HO : object_of F = object_of G
       & transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d))
                   HO
                   (morphism_of F)
         = morphism_of G }
         (only parsing).
  Definition path_functor'_sig (F G : Functor C D) : path_functor'_T F G -> F = G.
  Proof.
    intros [H' H''].
    destruct F, G; simpl in *.
    induction H'. (* while destruct H' works *) destruct H''.
    apply ap11; [ apply ap | ];
    apply center; abstract exact _.
    Set Printing Universes.
    (* Fail Defined.*)
  (* The command has indeed failed with message:
=> Error: path_functor'_sig_subproof already exists. *)
  Defined.
(* Anomaly: Backtrack.backto 55: a state with no vcs_backup. Please report. *)
End path_functor.

quality98%

¤ Dauer der Verarbeitung: 0.5 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.