(*|
点付き型
========
|*)

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.
Proof.
  unshelve econstructor.
  -
    exact (fun A => A).
  -
    simpl.
    intros.
    exact (point_preserving X X0 f0).
  -
    simpl.
    intros.
    unfold point_preserving.
    reflexivity.
  -
    simpl.
    intros.
    unfold point_preserving in *.
    subst z.
    subst y.
    reflexivity.
Defined.