Skip to content

Instantly share code, notes, and snippets.

@jwiegley
Last active August 25, 2022 22:45
Show Gist options
  • Save jwiegley/0b1093c687e392f02a478f96b98db11f to your computer and use it in GitHub Desktop.
Save jwiegley/0b1093c687e392f02a478f96b98db11f to your computer and use it in GitHub Desktop.
Definition Domain (A : Type) := A → Prop.
Axiom Domain_irrelevance :
∀ {A : Type} (P : Domain A) (x : A) (H1 H2 : P x), H1 = H2.
Program Definition Par : Category := {|
obj := Type;
hom := fun A B => { D : Domain A & ∀ x : A, D x → B };
homset := fun P Q => {|
equiv := fun '(Df; f) '(Dg; g) =>
∀ x (df : Df x) (dg : Dg x), f x df = g x dg
|};
id := λ _, (λ _, True; λ x _, x);
compose := fun _ _ _ '(Df; f) '(Dg; g) => _
|}.
Next Obligation.
equivalence; subst.
- now pose proof (Domain_irrelevance _ _ df dg); subst.
- (* stuck, missing D for the transitive term *)
Import EqNotations.
Program Definition Par : Category := {|
obj := Type;
hom := fun A B => { D : Ensemble A & ∀ x : A, D x → B };
homset := fun _ _ => {|
equiv := fun '(Df; f) '(Dg; g) =>
{ S : Same_set _ Df Dg
| ∀ x (df : Df x),
f x df = g x (rew (Extensionality_Ensembles _ _ _ S) in df) }
|};
id := λ _, (λ _, True; λ x _, x);
compose := fun _ _ _ '(Df; f) '(Dg; g) => _
|}.
Import EqNotations.
Program Definition Par : Category := {|
obj := obj[Sets];
hom := fun A B => ∃ D : obj[Sets], D ~> A × B;
homset := fun _ _ => {|
equiv := fun '(Df; f) '(Dg; g) => ∀ iso : Df ≅ Dg, f ≈ g ∘ iso
|};
id := λ A, (A; {| morphism := λ x : A, _ |});
compose := fun _ _ _ '(Df; f) '(Dg; g) => _
|}.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment