|
(* File reduced by coq-bug-finder from original input, then from 9492 lines to 119 lines *)
(* coqc version 8.5beta1 (January 2015) compiled on Jan 18 2015 7:27:36 with OCaml 3.12.1
coqtop version 8.5beta1 (January 2015) *)
Set Typeclasses Dependency Order.
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y" := (@paths _ x y) : type_scope.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with idpath => idpath end.
Set Implicit Arguments.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope object_scope with object.
Record PreCategory := Build_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' }.
Arguments identity {!C%category} / x%object : rename.
Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename.
Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := {
morphism_inverse : morphism C d s;
left_inverse : compose morphism_inverse m = identity _;
right_inverse : compose m morphism_inverse = identity _ }.
Arguments morphism_inverse {C s d} m {_}.
Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope.
Class Isomorphic {C : PreCategory} s d := {
morphism_isomorphic :> morphism C s d;
isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
Coercion morphism_isomorphic : Isomorphic >-> morphism.
Variable C : PreCategory.
Variables s d : C.
Definition path_isomorphic (i j : Isomorphic s d)
: @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j -> i = j.
Admitted.
Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q
: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
Abort.
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
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.
|
