Dependent equality in Coq

Question

Let’s say that cat is the type of categories (I don’t think its precise formalization really matters here). I define the type of « initial structures » of a category ℭ as follows:

Record weak_initial := {
  w_initial_obj :> obj ℭ;
  arrow0D (D : obj ℭ) : hom w_initial_obj D;
}.
 
Record initial := {
  w_initial :> weak_initial;
  initialP : ∀ {D} (f : hom w_initial D), f = arrow0D w_initial D;
}.

I can show:

Lemma eq_initial : ∀ (p q : initial), w_initial p = w_initial q -> 
  p = q. 

In « usual » mathematics we have something stronger:

 ∀ (p q : initial), w_initial_obj p = w_initial_obj q -> 
  p = q. 

I don’t think this is provable because we don’t have functional extensionality. I don’t see how to define initial structures in such a way that this statement would be provable. Anyway, given two initial structures on the same object and some object D:

Variable initial1 initial2 : initial. 
Variable P : w_initial_obj initial1 = w_initial_obj initial2.
Variable D : ℭ. 

I can prove

Lemma equal_homs : eq_rect (w_initial_obj initial1)
      (λ _ : ℭ, Type)
      (hom (w_initial_obj initial1) D)
      (w_initial_obj initial2) P =
    hom (w_initial_obj initial2) D.

but can we prove a statement that relates arrow0D initial1 D and arrow0D initial2 D?

Answer 1

Given p : initial and q : initial, you can relate arrow0D p D : hom (w_initial_obj p) D to arrow0D q D : hom (w_initial_obj q) D by transporting the former along equal_homs and equating the result with arrow0D q D. That is to say, you can prove (after unfolding a proof of equal_homs):

forall {D},
  eq_rect (w_initial_obj p) (fun ini => hom ini D)
    (arrow0D p D) (w_initial_obj q) w_initial_obj_eq
  = (arrow0D q D)

---

Full code:

Set Implicit Arguments.
Set Contextual Implicit.

Record category := {
  obj : Type;
  hom : obj -> obj -> Type;
}.

Arguments hom {_}.

Section C.

Context (ℭ : category).

Record weak_initial := {
  w_initial_obj :> obj ℭ;
  arrow0D (D : obj ℭ) : hom w_initial_obj D;
}.
 
Record initial := {
  w_initial :> weak_initial;
  initialP : forall {D} (f : hom w_initial D), f = arrow0D w_initial D;
}.

(* ad hoc equality of initial objects *)
Record initial_eq (p q : initial) : Prop := {
  w_initial_obj_eq : w_initial_obj p = w_initial_obj q;
  (* (arrow0D p D) equals (arrow0D q D) modulo transport along w_initial_obj_eq *)
  arrow0D_eq : forall {D}, eq_rect (w_initial_obj p) (fun ini => hom ini D) (arrow0D p D) (w_initial_obj q) w_initial_obj_eq = (arrow0D q D);
}.

Lemma initial_unique : forall (p q : initial), w_initial_obj p = w_initial_obj q -> 
  initial_eq p q.
Proof.
  intros p q e.
  destruct p as [[? ?] initialPp]; destruct q as [[? ?] ?]; cbn in *.
  destruct e; cbn in *.
  unshelve econstructor; cbn.
  - reflexivity.
  - intros D. rewrite initialPp. reflexivity.
Qed.

End C.
```

Answer 2

Indeed, I do not think you will be able to get any further without function extensionality (and possibly proposition extensionality, too – without it, there is also no reason that different proofs of the same equality, such as your initialP be equal).

There are many libraries for category theory out there, both in Coq and other proof assistants. Unless you want specifically to try something new, I would recommend trying to take inspiration from those. It might seem at first that category theory would be an easy field to formalise, but experience seems to indicate it is much harder than one would expect – in part because of such issues of "what equality is".