点付き型

Require Import category.

Set Implicit Arguments.

Record pointed_type : Type :=
  make_pointed_type {
    A    :> Type;
    base :  A;
  }.

Definition point_preserving
  (A B : Type)
  (a0 : A)
  (b0 : B)
  (f : A -> B)
  : Prop :=
    f a0 = b0.

Record point_preserving_map
  (A B : pointed_type)
  : Type :=
  make_point_preserving_map {
    f                     :> A -> B;
    f_is_point_preserving :> point_preserving A.(base) B.(base) f;
  }.

Definition displayed_category_of_pointed_types
  : displayed_category_data category_of_types_data.displayed_category_data category_of_types_data
Proof.displayed_category_data category_of_types_data
  unshelve econstructor.category_of_types_data -> Type
forall a b : category_of_types_data,
category_of_types_data [a, b] -> ?d_ob a -> ?d_ob b -> Type
forall (a : category_of_types_data) (x : ?d_ob a), ?d_hom a a id x x
forall (a b c : category_of_types_data) (x : ?d_ob a) 
  (y : ?d_ob b) (z : ?d_ob c) (g : category_of_types_data [b, c])
  (f0 : category_of_types_data [a, b]),
?d_hom b c g y z -> ?d_hom a b f0 x y -> ?d_hom a c (g ∘ f0) x z
  -category_of_types_data -> Type
    exact (fun A => A).
  -forall a b : category_of_types_data,
category_of_types_data [a, b] ->
(fun A : category_of_types_data => A) a ->
(fun A : category_of_types_data => A) b -> Type
    simpl.forall a b : Type, (a -> b) -> a -> b -> Type
    intros.a, b: Type
f0: a -> b
X: a
X0: b
Type
    exact (point_preserving X X0 f0).
  -forall (a : category_of_types_data)
  (x : (fun A : category_of_types_data => A) a),
((fun (a0 b : Type) (f0 : a0 -> b) (H : a0) (H0 : b) =>
  point_preserving H H0 f0)
 :
 forall a0 b : category_of_types_data,
 category_of_types_data [a0, b] ->
 (fun A : category_of_types_data => A) a0 ->
 (fun A : category_of_types_data => A) b -> Type) a a id x x
    simpl.forall (a : Type) (x : a), point_preserving x x (fun x0 : a => x0)
    intros.a: Type
x: a
point_preserving x x (fun x0 : a => x0)
    unfold point_preserving.a: Type
x: a
x = x
    reflexivity.
  -forall (a b c : category_of_types_data)
  (x : (fun A : category_of_types_data => A) a)
  (y : (fun A : category_of_types_data => A) b)
  (z : (fun A : category_of_types_data => A) c)
  (g : category_of_types_data [b, c]) (f0 : category_of_types_data [a, b]),
((fun (a0 b0 : Type) (f : a0 -> b0) (H : a0) (H0 : b0) =>
  point_preserving H H0 f)
 :
 forall a0 b0 : category_of_types_data,
 category_of_types_data [a0, b0] ->
 (fun A : category_of_types_data => A) a0 ->
 (fun A : category_of_types_data => A) b0 -> Type) b c g y z ->
((fun (a0 b0 : Type) (f : a0 -> b0) (H : a0) (H0 : b0) =>
  point_preserving H H0 f)
 :
 forall a0 b0 : category_of_types_data,
 category_of_types_data [a0, b0] ->
 (fun A : category_of_types_data => A) a0 ->
 (fun A : category_of_types_data => A) b0 -> Type) a b f0 x y ->
((fun (a0 b0 : Type) (f1 : a0 -> b0) (H : a0) (H0 : b0) =>
  point_preserving H H0 f1)
 :
 forall a0 b0 : category_of_types_data,
 category_of_types_data [a0, b0] ->
 (fun A : category_of_types_data => A) a0 ->
 (fun A : category_of_types_data => A) b0 -> Type) a c 
  (g ∘ f0) x z
    simpl.forall (a b c : Type) (x : a) (y : b) (z : c) (g : b -> c) (f0 : a -> b),
point_preserving y z g ->
point_preserving x y f0 -> point_preserving x z (fun x0 : a => g (f0 x0))
    intros.a, b, c: Type
x: a
y: b
z: c
g: b -> c
f0: a -> b
g': point_preserving y z g
f': point_preserving x y f0
point_preserving x z (fun x0 : a => g (f0 x0))
    unfold point_preserving in *.a, b, c: Type
x: a
y: b
z: c
g: b -> c
f0: a -> b
g': g y = z
f': f0 x = y
g (f0 x) = z
    subst z.a, b, c: Type
x: a
y: b
g: b -> c
f0: a -> b
f': f0 x = y
g (f0 x) = g y
    subst y.a, b, c: Type
x: a
g: b -> c
f0: a -> b
g (f0 x) = g (f0 x)
    reflexivity.
Defined.