At the bottom of the post you can find a formalization of “setoids” and “setoid morphisms” (nothing fancy except it’s u-polymorphic: but I am still on Coq 8.18 – and please don’t mind the naming too much, this is all still draft level).
With those definitions, I can e.g. start formalizing “wild categories” (by which I just mean that Ob and Mor are arbitrary “setoids”), and, in particular, I can make dom/cod “setoid morphisms”:
(** The type of "category data". *)
Structure CatData@{i o} : Type@{o} :=
mkCatData {
Ob : ESet@{i o};
Mor : ESet@{i o};
dom : Mor --> Ob;
cod : Mor --> Ob;
} as Cd.
Arguments dom {Cd}.
Arguments cod {Cd}.
Notation "x '=o=' y" := (weqv (eeqv (Ob _)) x y)
(at level 70, no associativity).
Notation "f '=m=' g" := (weqv (eeqv (Mor _)) f g)
(at level 70, no associativity).
Definition Hom@{i o} Cd (x y : Ob@{i o} Cd) : Type@{o} :=
{f : Mor Cd |- dom f =o= x /\ cod f =o= y}. (** u-poly as [psig] *)
Definition HomEqv@{i o} Cd (w x y z : Ob@{i o} Cd)
(fH : Hom w x) (gH : Hom y z) : Prop :=
psig_pi1@{i o} fH =m= psig_pi1@{i o} gH.
(* etc. etc. *)
But later (I think) I get to need the dependent version of “setoid morphisms”, e.g. here:
(** The type of "functor data" from [B] to [C]. *)
Structure FunData@{i o} (B C : Cat@{i o}) : Type@{o} :=
mkFunData {
fOb : Ob B --> Ob C;
fMor : forall (f : Mor B), (** not yet a (dep.) morphism: but what is that? *)
Hom (fOb (dom f)) (fOb (cod f));
} as Fd.
(I am not showing the whole code up to Cat to try and keep things short: but let me know if you’d rather want me to post it.)
That much for motivation. I’d have two questions:
-
incidentally, am I right that I need “setoid morphisms”, not just “functions” for a formalization of these “wild categories” that is faithful and also works down the line?
-
but, especially, I (seem to) get to needing a dependent version of “setoid morphisms”, but how should I formulate it?
This is what I have started writing, beginning with the idea that wfor must be a “dependent function”, but then wfor_prop doesn’t seem to make much sense, as it lands in two distinct WSets, FT x and FT y, so I seem to be missing some piece, maybe some kind of higher-order equivalence…?
(** The type of "dep. pre-morphisms" between [WSet]s with [WEqv]. *)
Structure WFor@{i o} (S : WSet@{i o}) (FT : S -> WSet@{i o})
(ES : WEqv@{i o} S) (EFT : forall x, WEqv@{i o} (FT x)) : Type@{o} :=
mkWFor {
(** The "operation". *)
wfor :> forall x, FT x;
(** [wfor] is "coherent" with [weqv]. *)
wfor_prop : forall x y,
weqv ES x y -> weqv _ (wfor x) (wfor y); (** this fails *)
} as FFT.
I have also looked at the definition of respectful_hetero from the StdLib, but I cannot figure out if/how it would apply.
I think I am just missing the point somewhere: any help would be very much appreciated.
Thank you.
(********************************************************************)
(** ** SETUP *)
(********************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Strongly Strict Implicit.
Unset Contextual Implicit.
Unset Reversible Pattern Implicit.
Unset Printing Implicit Defensive.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Set Cumulativity Weak Constraints.
Unset Universe Minimization ToSet.
Set Primitive Projections.
(********************************************************************)
(** ** Pre-sets *)
(********************************************************************)
(** The type of "pre-sets". *)
Structure WSet@{i o} : Type@{o} :=
mkWSet {
wset :> Type@{i};
} as S.
(** The type of "pre-relations" on a [WSet]. *)
Definition WRel@{i o} (S : WSet@{i o}) : Type@{o} :=
S -> S -> Prop.
(** Represents "is reflexive" of a [WRel]. *)
Definition WRelRefl@{i o} S (RS : WRel@{i o} S) : Type@{o} :=
forall x, RS x x.
(** Represents "is symmetric" of a [WRel]. *)
Definition WRelSymm@{i o} S (RS : WRel@{i o} S) : Type@{o} :=
forall x y, RS x y -> RS y x.
(** Represents "is transitive" of a [WRel]. *)
Definition WRelTran@{i o} S (RS : WRel@{i o} S) : Type@{o} :=
forall x y z, RS x y -> RS y z -> RS x z.
(** The type of "pre-equivalences" on a [WSet]. *)
Structure WEqv@{i o} (S : WSet@{i o}) : Type@{o} :=
mkWEqv {
(** The "predicate". *)
weqv :> WRel@{i o} S;
(** [weq] is "reflexive". *)
weqv_refl : WRelRefl weqv;
(** [weq] is "symmetric". *)
weqv_symm : WRelSymm weqv;
(** [weq] is "transitive". *)
weqv_tran : WRelTran weqv;
} as ES.
(** The type of "pre-morphisms" between [WSet]s with [WEqv]. *)
Structure WMor@{i o} S T (ES : WEqv@{i o} S)
(ET : WEqv@{i o} T) : Type@{o} :=
mkWMor {
(** The "operation". *)
wfun :> S -> T;
(** [wfun] is "coherent" with [weqv]. *)
wfun_prop : forall x y,
weqv ES x y -> weqv ET (wfun x) (wfun y);
} as MST.
(********************************************************************)
(** ** Setoids *)
(********************************************************************)
(** The type of "setoids". *)
Structure ESet@{i o} : Type@{o} :=
mkESet {
eset :> WSet@{i o};
eeqv : WEqv@{i o} eset;
} as S.
(** The type of "setoid morphisms". *)
Definition EMor@{i o} (S T : ESet@{i o}) : Type@{o} :=
WMor@{i o} (eeqv S) (eeqv T).
Notation "S '-->' T" := (EMor S T)
(at level 99, no associativity).