Set Implicit Arguments.

Section PublicService.

  Inductive False : Type :=.

  Definition Not (P : Type) := P -> False.

  Inductive True : Type :=
  | I : True.

  Inductive Identity (T : Type) (t : T) : T -> Type :=
  | identical : Identity t t.

  Inductive And (P Q : Type) : Type :=
  | both : P -> Q -> And P Q.
  Definition proj1 {P Q} (a : And P Q) : P :=
    match a with both p q => p end.
  Definition proj2 {P Q} (a : And P Q) : Q :=
    match a with both p q => q end.

  Definition And_idem (P : Type) : P -> And P P.
  intro p; apply (both p p).
  Defined.

  Inductive Or (P Q : Type) : Type :=
  | inleft : P -> Or P Q
  | inright : Q -> Or P Q.

  Definition Decidable (P : Type) := Or P (Not P).

  Inductive Sigma (T : Type) (P : T -> Type) : Type :=
  | witness : forall t : T, P t -> Sigma P.
  Definition pi1 {T P} (s : @Sigma T P) : T :=
    match s with
      | witness t _ => t
    end.

  Definition Relation (T : Type) := T -> T -> Type.

  Record Equivalence {T : Type} (R : Relation T)
    := { equivalence_reflexivity : forall x, R x x
       ; equivalence_symmetry : forall x y, R x y -> R y x
       ; equivalence_transitivity : forall x y z, R x y -> R y z -> R x z
       }.

  Theorem Equivalence_Identity {T : Type} : Equivalence (@Identity T).
  apply Build_Equivalence.
  intros x; apply identical.
  intros x y; intro E; elim E; apply identical.
  intros x y z; intros E F; elim F; elim E; apply identical.
  Defined.

  Theorem Equivalence_Identity_Pullback {X T : Type} (f : X -> T) : Equivalence (fun x x' => @Identity T (f x) (f x')).
  apply Build_Equivalence.
  intros x; apply identical.
  intros x y; intro E; elim E; apply identical.
  intros x y z; intros E F; elim F; elim E; apply identical.
  Defined.

End PublicService.

Section CategoryTheory.

Record Category
  (Ob : Type)
  (Hom : Ob -> Ob -> Type)
  (Hom_eq : forall X Y, Relation (Hom X Y))

  := { identity : forall X, Hom X X
     ; compose : forall X Y Z, Hom X Y -> Hom Y Z -> Hom X Z
     ; compose_respectful_left : forall X Y Z (f f' : Hom X Y) (g : Hom Y Z),
       Hom_eq _ _ f f' ->
       Hom_eq _ _ (compose f g) (compose f' g)
     ; compose_respectful_right : forall X Y Z (f : Hom X Y) (g g' : Hom Y Z),
       Hom_eq _ _ g g' ->
       Hom_eq _ _ (compose f g) (compose f g')
     ; category_equivalence : forall X Y, Equivalence (Hom_eq X Y)
     ; category_left_identity : forall X Y (f : Hom X Y),
       Hom_eq _ _ (compose (identity _) f) f
     ; category_right_identity : forall X Y (f : Hom X Y),
       Hom_eq _ _ (compose f (identity _)) f
     ; category_associativity : forall X Y Z W (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W),
       Hom_eq _ _ (compose f (compose g h))
                  (compose (compose f g) h)
     }.

Notation "f '[' C ']'  g" := (compose C _ _ _ f g) (at level 20).
Notation "'Id[' C ']'" := (identity C _) (at level 20).

End CategoryTheory.

Section Functor.
  Context {C_Ob C_Hom C_Hom_eq} (C : @Category C_Ob C_Hom C_Hom_eq).
  Context {D_Ob D_Hom D_Hom_eq} (D : @Category D_Ob D_Hom D_Hom_eq).

  Record Functor
    := { Map_Ob : C_Ob -> D_Ob
       ; Map_Hom : forall X Y,
         C_Hom X Y -> D_Hom (Map_Ob X) (Map_Ob Y)
       ; functor_identity : forall X,
         D_Hom_eq (Map_Hom (identity C X)) (identity D (Map_Ob X))
       ; functor_compose : forall X Y Z (f : C_Hom X Y) (g : C_Hom Y Z),
         D_Hom_eq (Map_Hom (compose C _ _ _ f g)) (compose D _ _ _ (Map_Hom f) (Map_Hom g))
       ; Map_Hom_respectful : forall X Y (f f' : C_Hom X Y),
         C_Hom_eq f f' -> D_Hom_eq (Map_Hom f) (Map_Hom f')
    }.

  Notation "F '@' x" := (Map_Ob F x) (at level 20).
  Notation "F '$' f" := (Map_Hom F f) (at level 20).

  (*
  Theorem Functor_Map_Equation (F : Functor) {X Y} (f g : C_Hom X Y) : C_Hom_eq f g -> D_Hom_eq (Map_Hom F f) (Map_Hom F g).
    intro E.
    *)

End Functor.

Section SYMBOLIC.
  Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).

  Inductive Syntax : Ob -> Ob -> Type :=
  | idSYM : forall X : Ob, Syntax X X
  | compSYM : forall X Y Z : Ob, Syntax X Y -> Syntax Y Z -> Syntax X Z
  | injSYM : forall X Y, Hom X Y -> Syntax X Y.

  Inductive Semantics : Ob -> Ob -> Type :=
  | nilSYM : forall X : Ob, Semantics X X
  | consSYM : forall X Y Z : Ob, Hom X Y -> Semantics Y Z -> Semantics X Z.

  Fixpoint append {X Y Z : Ob} (f : Semantics X Y) : Semantics Y Z -> Semantics X Z :=
  match f with
    | nilSYM _ => fun g => g
    | consSYM _ _ _ s f => fun g => consSYM s (append f g)
  end.

  Lemma append_nil :
    forall (X Y : Ob) (x : Semantics X Y),
      Identity (append x (nilSYM Y)) x.
    induction x; simpl.
    apply identical.
    elim (equivalence_symmetry Equivalence_Identity _ _ IHx).
    apply identical.
  Defined.

  Lemma append_associative :
  forall (X Y Z W : Ob) (f : Semantics X Y) (g : Semantics Y Z) (h : Semantics Z W),
    Identity (append f (append g h))
             (append (append f g) h).
    intros; induction f; simpl.
    apply identical.
    elim (IHf _).
    apply identical.
  Defined.

  Fixpoint evalSYN {X Y} (s : Syntax X Y) : Semantics X Y :=
    match s with
      | idSYM _ => nilSYM _
      | compSYM _ _ _ f g => append (evalSYN f) (evalSYN g)
      | injSYM _ _ f => consSYM f (nilSYM _)
    end.

  Fixpoint quoteSYN {X Y} (s : Semantics X Y) : Syntax X Y :=
    match s with
      | nilSYM _ => idSYM _
      | consSYM _ _ _ f s => compSYM (injSYM f) (quoteSYN s)
    end.

  Definition Syntax_eq {X Y : Ob} (f f' : Syntax X Y) :=
    Identity (evalSYN f) (evalSYN f').
  Theorem Equivalence_Syntax_eq {X Y} : Equivalence (@Syntax_eq X Y).
    apply (Equivalence_Identity_Pullback evalSYN).
  Defined.

  Definition SYNTAX_category : Category Syntax (@Syntax_eq).
  apply (Build_Category Syntax (@Syntax_eq)
    idSYM
    compSYM); unfold Syntax_eq; simpl.
  intros X Y Z f f' g E; elim E; apply identical.
  intros X Y Z f g g' E; elim E; apply identical.
  intros X Y; apply Equivalence_Syntax_eq.
  intros X Y f; apply identical.
  intros X Y f; apply append_nil.
  intros X Y Z W f g h; apply append_associative.
  Defined.

  Theorem quote_eval_equal {X Y : Ob} (f : Syntax X Y) :
    Syntax_eq (quoteSYN (evalSYN f)) f.
    induction f; simpl in *;
      try apply identical.

    Lemma quote_eval_equal_lemma {X Y Z} (e1 : Semantics X Y) (e2 : Semantics Y Z) :
      Syntax_eq (quoteSYN (append e1 e2)) (compSYM (quoteSYN e1) (quoteSYN e2)).
      intros; induction e1; simpl.
      apply identical.
      elim (IHe1 e2).
      eapply (equivalence_transitivity (category_equivalence SYNTAX_category _ _)).
      Focus 2.
      apply (category_associativity SYNTAX_category _ _).
      apply (compose_respectful_right SYNTAX_category).
      apply IHe1.
    Defined.

    eapply (equivalence_transitivity Equivalence_Syntax_eq).
    apply quote_eval_equal_lemma.
    eapply (equivalence_transitivity (category_equivalence SYNTAX_category _ _)).
    apply (compose_respectful_left SYNTAX_category).
    apply IHf1.
    eapply (equivalence_transitivity (category_equivalence SYNTAX_category _ _)).
    apply (compose_respectful_right SYNTAX_category).
    apply IHf2.
    apply (equivalence_reflexivity (category_equivalence SYNTAX_category _ _)).
  Defined.

  Fixpoint interpret_Syntax {X Y} (f : Syntax X Y) : Hom X Y :=
    match f with
      | idSYM _ => identity C _
      | compSYM _ _ _ f g => compose C _ _ _ (interpret_Syntax f) (interpret_Syntax g)
      | injSYM _ _ f => f
    end.

  Fixpoint interpret_Semantics {X Y} (f : Semantics X Y) : Hom X Y :=
    match f with
      | nilSYM _ => identity C _
      | consSYM _ _ _ s f => compose C _ _ _ s (interpret_Semantics f)
    end.

  Theorem interpretation_factors_through_evaluation {X Y} (f : Syntax X Y) :
    Hom_eq (interpret_Syntax f)
           (interpret_Semantics (evalSYN f)).
    induction f; simpl.
    apply (equivalence_reflexivity (category_equivalence C _ _)).
    eapply (equivalence_transitivity (category_equivalence C _ _)).
    apply compose_respectful_left.
    apply IHf1.
    eapply (equivalence_transitivity (category_equivalence C _ _)).
    apply compose_respectful_right.
    apply IHf2.
    Lemma append_pushthrough_compose {X Y Z} (f : Semantics X Y) (g : Semantics Y Z) :
      Hom_eq (compose C _ _ _ (interpret_Semantics f) (interpret_Semantics g))
             (interpret_Semantics (append f g)).
      induction f; simpl.
      apply category_left_identity.
      eapply (equivalence_transitivity (category_equivalence C _ _)).
      apply (equivalence_symmetry (category_equivalence C _ _)).
      apply (category_associativity C).
      apply compose_respectful_right.
      apply IHf.
    Defined.
    apply append_pushthrough_compose.

    apply (equivalence_symmetry (category_equivalence C _ _)).
    apply category_right_identity.
  Defined.

  Definition Interpret : Functor SYNTAX_category C.
  Print Build_Functor.
  apply (Build_Functor
    SYNTAX_category C
    (fun X => X)
    (fun X Y f => interpret_Syntax f)
  ).

  intros; apply (equivalence_reflexivity (category_equivalence C _ _)).
  intros; apply (equivalence_reflexivity (category_equivalence C _ _)).

  intros X Y f f' E.
  pose (quote_eval_equal f) as A.
  pose (quote_eval_equal f') as B.
  pose (interpretation_factors_through_evaluation f) as U.
  pose (interpretation_factors_through_evaluation f') as V.
  unfold Syntax_eq in *.
  assert (
    Hom_eq (interpret_Syntax f) (interpret_Semantics (evalSYN f'))
  ) as P.
  elim E.
  assumption.
  eapply (equivalence_transitivity (category_equivalence C _ _)).
  apply P.
  apply (equivalence_symmetry (category_equivalence C _ _)).
  apply V.
  Defined.

End SYMBOLIC.

Section IsomorphismSubcategory.
  Context {Ob Hom Hom_eq} (C : @Category Ob Hom Hom_eq).

  Definition Isomorphism (X Y : Ob) :=
    @Sigma (And (Hom X Y) (Hom Y X))
    (fun (fg : And (Hom X Y) (Hom Y X)) =>
      match fg with
        | both f g =>
          And (Hom_eq (compose C _ _ _ f g) (identity C _))
              (Hom_eq (compose C _ _ _ g f) (identity C _))
        end).

  Definition Identity_Isomorphism (X : Ob) : Isomorphism X X.
  apply (witness _ (both (identity C X) (identity C X))).
  apply And_idem.
  apply category_left_identity.
  Defined.

  Definition Compose_Isomorphism (X Y Z : Ob)
    (f : Isomorphism X Y) (g : Isomorphism Y Z) :
    Isomorphism X Z.
  unfold Isomorphism in *.
  destruct f as [[fTo fFrom] [fPrf fPrf']].
  destruct g as [[gTo gFrom] [gPrf gPrf']].
  apply (witness _ (both (compose C _ _ _ fTo gTo)
                         (compose C _ _ _ gFrom fFrom))).
  apply both.

  pose (@SYNTAX_category Ob Hom) as SYN.
  assert (
    Syntax_eq
     (compose SYN X Z X (compose SYN X Y Z (injSYM _ _ fTo) (injSYM _ _ gTo)) (compose SYN Z Y X (injSYM _ _ gFrom) (injSYM _ _ fFrom)))
     (compose SYN _ _ _ (injSYM _ _ fTo)
       (compose SYN _ _ _
         (compose SYN _ _ _ (injSYM _ _ gTo) (injSYM _ _ gFrom))
         (injSYM _ _ fFrom)))
  ) as EQUATION by apply identical.
  pose (Map_Hom_respectful (Interpret C) _ _ _ _ EQUATION) as EQUATION'; simpl in EQUATION'.

  eapply (equivalence_transitivity (category_equivalence C _ _)).
  apply EQUATION'.
  clear EQUATION'; clear EQUATION.

  eapply (equivalence_transitivity (category_equivalence C _ _)).
  apply compose_respectful_right.
  apply compose_respectful_left.
  apply gPrf.

  eapply (equivalence_transitivity (category_equivalence C _ _)).
  apply compose_respectful_right.
  apply category_left_identity.
  apply fPrf.