Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: Coq

Original von: Coq^©

Unset Strict Universe Declaration.
Module Version1.
  Set Implicit Arguments.
  Set Universe Polymorphism.
  Generalizable All Variables.

  Record SpecializedCategory (obj : Type) :=
    {
      Object :> _ := obj
    }.

  Record > Category :=
    {
      CObject : Type;
      UnderlyingCategory :> @SpecializedCategory CObject
    }.

  Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
    {
      ObjectOf :> objC -> objD
    }.

  Definition Functor (C D : Category) := SpecializedFunctor C D.

  Parameter TerminalCategory : SpecializedCategory unit.

  Definition focus A (_ : A) := True.

  Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
    assert (Hf : focus ((S tt) = (S tt))) by constructor.
    let C1 := constr:(CObject) in
    let C2 := constr:(fun C => @Object (CObject C) C) in
    unify C1 C2; idtac C1 C2. Show Universes.
    progress change @CObject with (fun C => @Object (CObject C) C) in *.
    simpl in *.
    match type of Hf with
      | focus ?V => exact V
    end.
  Defined.

  Definition Build_SliceCategory (A : Category) (F : Functor TerminalCategory A) := @Build_SpecializedCategory (CommaCategory_Object F).
  Parameter SetCat : @SpecializedCategory Set.

  Set Printing Universes.
  Check (fun (A : Category) (F : Functor TerminalCategory A) => @Build_SpecializedCategory (CommaCategory_Object F)) SetCat.
  (* (fun (A : Category (* Top.68 *))
   (F : Functor (* Set Top.68 *) TerminalCategory A) =>
{|  |}) SetCat (* Top.68 *)
     : forall
         F : Functor (* Set Top.68 *) TerminalCategory SetCat (* Top.68 *),
       let Object := CommaCategory_Object (* Top.68 Top.69 Top.68 *) F in
       SpecializedCategory (* Top.69 *)
         (CommaCategory_Object (* Top.68 Top.69 Top.68 *) F) *)
  Check @Build_SliceCategory SetCat. (* Toplevel input, characters 0-34:
Error: Universe inconsistency (cannot enforce Top.51 <= Set because Set
< Top.51). *)
End Version1.

Module Version2.
  Set Implicit Arguments.
  Set Universe Polymorphism.

  Record SpecializedCategory (obj : Type) :=
    {
      Object : _ := obj
    }.

  Record > Category :=
    {
      CObject : Type;
      UnderlyingCategory :> @SpecializedCategory CObject
    }.

  Parameter TerminalCategory : SpecializedCategory unit.

  Definition focus A (_ : A) := True.
  Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
                               (objD : Type) (D : SpecializedCategory objD), Prop.
  Definition CommaCategory_Object (A : Category) : Type.
    assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
    progress change CObject with (fun C => @Object (CObject C) C) in *;
      simpl in *.
    match type of Hf with
      | focus ?V => exact V
    end.
  Defined.

  Definition Build_SliceCategory := @CommaCategory_Object.
  Parameter SetCat : @SpecializedCategory Set.

  Set Printing Universes.
  Check @Build_SliceCategory SetCat.
End Version2.

Module OtherBug.
  Set Implicit Arguments.
  Set Universe Polymorphism.

  Record SpecializedCategory (obj : Type) :=
    {
      Object : _ := obj
    }.

  Record > Category :=
    {
      CObject : Type;
      UnderlyingCategory :> @SpecializedCategory CObject
    }.

  Parameter TerminalCategory : SpecializedCategory unit.

  Definition focus A (_ : A) := True.

  Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
                               (objD : Type) (D : SpecializedCategory objD), Prop.
  Definition CommaCategory_Object (A : Category@{i}) : Type.
    assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
    progress change CObject with (fun C => @Object (CObject C) C) in *;
      simpl in *.
    match type of Hf with
      | focus ?V => exact V
    end.
  Defined.

  Parameter SetCat : @SpecializedCategory Set.

  Set Printing Universes.
  Definition Build_SliceCategory := @CommaCategory_Object.
  Check @CommaCategory_Object SetCat.
  (* CommaCategory_Object (* Top.43 Top.44 Top.43 *) SetCat (* Top.43 *)
     : Type (* Top.44 *) *)
  Check @Build_SliceCategory SetCat.
  (* Toplevel input, characters 0-34:
Error: Universe inconsistency (cannot enforce Top.36 <= Set because Set
< Top.36). *)
End OtherBug.

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