Library HoTT.WildCat.Displayed
Require Import Basics.Overture.
Require Import Basics.PathGroupoids.
Require Import Basics.Tactics.
Require Import Types.Sigma.
Require Import WildCat.Core.
Require Import WildCat.Prod.
Class IsDGraph {A : Type} `{IsGraph A} (D : A → Type)
:= DHom : ∀ {a b : A}, (a $-> b) → D a → D b → Type.
Class IsD01Cat {A : Type} `{Is01Cat A} (D : A → Type) `{!IsDGraph D} :=
{
DId : ∀ {a : A} (a' : D a), DHom (Id a) a' a';
dcat_comp : ∀ {a b c : A} {g : b $-> c} {f : a $-> b}
{a' : D a} {b' : D b} {c' : D c},
DHom g b' c' → DHom f a' b' → DHom (g $o f) a' c';
}.
Notation "g '$o'' f" := (dcat_comp g f).
Definition dcat_postcomp {A : Type} {D : A → Type} `{IsD01Cat A D} {a b c : A}
{g : b $-> c} {a' : D a} {b' : D b} {c' : D c} (g' : DHom g b' c')
: ∀ (f : a $-> b), DHom f a' b' → DHom (g $o f) a' c'
:= fun _ f' ⇒ g' $o' f'.
Definition dcat_precomp {A : Type} {D : A → Type} `{IsD01Cat A D} {a b c : A}
{f : a $-> b} {a' : D a} {b' : D b} {c' : D c} (f' : DHom f a' b')
: ∀ (g : b $-> c), DHom g b' c' → DHom (g $o f) a' c'
:= fun _ g' ⇒ g' $o' f'.
Class IsD0Gpd {A : Type} `{Is0Gpd A} (D : A → Type)
`{!IsDGraph D, !IsD01Cat D}
:= dgpd_rev : ∀ {a b : A} {f : a $== b} {a' : D a} {b' : D b},
DHom f a' b' → DHom (f^$) b' a'.
Notation "p ^$'" := (dgpd_rev p).
Definition DGpdHom {A : Type} {D : A → Type} `{IsD0Gpd A D} {a b : A}
(f : a $== b) (a' : D a) (b' : D b)
:= DHom f a' b'.
Require Import Basics.PathGroupoids.
Require Import Basics.Tactics.
Require Import Types.Sigma.
Require Import WildCat.Core.
Require Import WildCat.Prod.
Class IsDGraph {A : Type} `{IsGraph A} (D : A → Type)
:= DHom : ∀ {a b : A}, (a $-> b) → D a → D b → Type.
Class IsD01Cat {A : Type} `{Is01Cat A} (D : A → Type) `{!IsDGraph D} :=
{
DId : ∀ {a : A} (a' : D a), DHom (Id a) a' a';
dcat_comp : ∀ {a b c : A} {g : b $-> c} {f : a $-> b}
{a' : D a} {b' : D b} {c' : D c},
DHom g b' c' → DHom f a' b' → DHom (g $o f) a' c';
}.
Notation "g '$o'' f" := (dcat_comp g f).
Definition dcat_postcomp {A : Type} {D : A → Type} `{IsD01Cat A D} {a b c : A}
{g : b $-> c} {a' : D a} {b' : D b} {c' : D c} (g' : DHom g b' c')
: ∀ (f : a $-> b), DHom f a' b' → DHom (g $o f) a' c'
:= fun _ f' ⇒ g' $o' f'.
Definition dcat_precomp {A : Type} {D : A → Type} `{IsD01Cat A D} {a b c : A}
{f : a $-> b} {a' : D a} {b' : D b} {c' : D c} (f' : DHom f a' b')
: ∀ (g : b $-> c), DHom g b' c' → DHom (g $o f) a' c'
:= fun _ g' ⇒ g' $o' f'.
Class IsD0Gpd {A : Type} `{Is0Gpd A} (D : A → Type)
`{!IsDGraph D, !IsD01Cat D}
:= dgpd_rev : ∀ {a b : A} {f : a $== b} {a' : D a} {b' : D b},
DHom f a' b' → DHom (f^$) b' a'.
Notation "p ^$'" := (dgpd_rev p).
Definition DGpdHom {A : Type} {D : A → Type} `{IsD0Gpd A D} {a b : A}
(f : a $== b) (a' : D a) (b' : D b)
:= DHom f a' b'.
Diagrammatic order to match gpd_comp
Definition dgpd_comp {A : Type} {D : A → Type} `{IsD0Gpd A D} {a b c : A}
{f : a $== b} {g : b $== c} {a' : D a} {b' : D b} {c' : D c}
: DGpdHom f a' b' → DGpdHom g b' c' → DGpdHom (g $o f) a' c'
:= fun f' g' ⇒ g' $o' f'.
Notation "p '$@'' q" := (dgpd_comp p q).
Definition DHom_path {A : Type} {D : A → Type} `{IsD01Cat A D} {a b : A}
(p : a = b) {a' : D a} {b': D b} (p' : transport D p a' = b')
: DHom (Hom_path p) a' b'.
Proof.
destruct p, p'; apply DId.
Defined.
Definition DGpdHom_path {A : Type} {D : A → Type} `{IsD0Gpd A D} {a b : A}
(p : a = b) {a' : D a} {b': D b} (p' : transport D p a' = b')
: DGpdHom (GpdHom_path p) a' b'
:= DHom_path p p'.
Global Instance reflexive_DHom {A} {D : A → Type} `{IsD01Cat A D} {a : A}
: Reflexive (DHom (Id a))
:= fun a' ⇒ DId a'.
Global Instance reflexive_DGpdHom {A} {D : A → Type} `{IsD0Gpd A D} {a : A}
: Reflexive (DGpdHom (Id a))
:= fun a' ⇒ DId a'.
{f : a $== b} {g : b $== c} {a' : D a} {b' : D b} {c' : D c}
: DGpdHom f a' b' → DGpdHom g b' c' → DGpdHom (g $o f) a' c'
:= fun f' g' ⇒ g' $o' f'.
Notation "p '$@'' q" := (dgpd_comp p q).
Definition DHom_path {A : Type} {D : A → Type} `{IsD01Cat A D} {a b : A}
(p : a = b) {a' : D a} {b': D b} (p' : transport D p a' = b')
: DHom (Hom_path p) a' b'.
Proof.
destruct p, p'; apply DId.
Defined.
Definition DGpdHom_path {A : Type} {D : A → Type} `{IsD0Gpd A D} {a b : A}
(p : a = b) {a' : D a} {b': D b} (p' : transport D p a' = b')
: DGpdHom (GpdHom_path p) a' b'
:= DHom_path p p'.
Global Instance reflexive_DHom {A} {D : A → Type} `{IsD01Cat A D} {a : A}
: Reflexive (DHom (Id a))
:= fun a' ⇒ DId a'.
Global Instance reflexive_DGpdHom {A} {D : A → Type} `{IsD0Gpd A D} {a : A}
: Reflexive (DGpdHom (Id a))
:= fun a' ⇒ DId a'.
A displayed 0-functor F' over a 0-functor F acts on displayed objects and 1-cells and satisfies no axioms.
Class IsD0Functor {A : Type} {B : Type}
{DA : A → Type} `{IsDGraph A DA} {DB : B → Type} `{IsDGraph B DB}
(F : A → B) `{!Is0Functor F} (F' : ∀ (a : A), DA a → DB (F a))
:= dfmap : ∀ {a b : A} {f : a $-> b} {a' : DA a} {b' : DA b},
DHom f a' b' → DHom (fmap F f) (F' a a') (F' b b').
Arguments dfmap {A B DA _ _ DB _ _} F {_} F' {_ _ _ _ _ _} f'.
Class IsD2Graph {A : Type} `{Is2Graph A}
(D : A → Type) `{!IsDGraph D}
:= isdgraph_hom : ∀ {a b} {a'} {b'},
IsDGraph (fun (f:a $-> b) ⇒ DHom f a' b').
Global Existing Instance isdgraph_hom.
#[global] Typeclasses Transparent IsD2Graph.
Class IsD1Cat {A : Type} `{Is1Cat A}
(D : A → Type) `{!IsDGraph D, !IsD2Graph D, !IsD01Cat D} :=
{
isd01cat_hom : ∀ {a b : A} {a' : D a} {b' : D b},
IsD01Cat (fun f ⇒ DHom f a' b');
isd0gpd_hom : ∀ {a b : A} {a' : D a} {b' : D b},
IsD0Gpd (fun f ⇒ DHom f a' b');
isd0functor_postcomp : ∀ {a b c : A} {g : b $-> c} {a' : D a}
{b' : D b} {c' : D c} (g' : DHom g b' c'),
@IsD0Functor _ _ (fun f ⇒ DHom f a' b')
_ _ (fun gf ⇒ DHom gf a' c')
_ _ (cat_postcomp a g) _ (dcat_postcomp g');
isd0functor_precomp : ∀ {a b c : A} {f : a $-> b} {a' : D a}
{b' : D b} {c' : D c} (f' : DHom f a' b'),
@IsD0Functor _ _ (fun g ⇒ DHom g b' c')
_ _ (fun gf ⇒ DHom gf a' c')
_ _ (cat_precomp c f) _ (dcat_precomp f');
dcat_assoc : ∀ {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
DHom (cat_assoc f g h) ((h' $o' g') $o' f')
(h' $o' (g' $o' f'));
dcat_assoc_opp : ∀ {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f'))
((h' $o' g') $o' f');
dcat_idl : ∀ {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
(f' : DHom f a' b'), DHom (cat_idl f) (DId b' $o' f') f';
dcat_idr : ∀ {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
(f' : DHom f a' b'), DHom (cat_idr f) (f' $o' DId a') f';
}.
Global Existing Instance isd01cat_hom.
Global Existing Instance isd0gpd_hom.
Global Existing Instance isd0functor_postcomp.
Global Existing Instance isd0functor_precomp.
Definition dcat_postwhisker {A : Type} {D : A → Type} `{IsD1Cat A D}
{a b c : A} {f g : a $-> b} {h : b $-> c} {p : f $== g}
{a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'}
(h' : DHom h b' c') (p' : DHom p f' g')
: DHom (h $@L p) (h' $o' f') (h' $o' g')
:= dfmap (cat_postcomp a h) (dcat_postcomp h') p'.
Notation "h $@L' p" := (dcat_postwhisker h p).
Definition dcat_prewhisker {A : Type} {D : A → Type} `{IsD1Cat A D}
{a b c : A} {f : a $-> b} {g h : b $-> c} {p : g $== h}
{a' : D a} {b' : D b} {c' : D c} {g' : DHom g b' c'} {h' : DHom h b' c'}
(p' : DHom p g' h') (f' : DHom f a' b')
: DHom (p $@R f) (g' $o' f') (h' $o' f')
:= dfmap (cat_precomp c f) (dcat_precomp f') p'.
Notation "p $@R' f" := (dcat_prewhisker p f).
Definition dcat_comp2 {A : Type} {D : A → Type} `{IsD1Cat A D} {a b c : A}
{f g : a $-> b} {h k : b $-> c} {p : f $== g} {q : h $== k}
{a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'}
{h' : DHom h b' c'} {k' : DHom k b' c'}
(p' : DHom p f' g') (q' : DHom q h' k')
: DHom (p $@@ q) (h' $o' f') (k' $o' g')
:= (k' $@L' p') $o' (q' $@R' f').
Notation "q $@@' p" := (dcat_comp2 q p).
{DA : A → Type} `{IsDGraph A DA} {DB : B → Type} `{IsDGraph B DB}
(F : A → B) `{!Is0Functor F} (F' : ∀ (a : A), DA a → DB (F a))
:= dfmap : ∀ {a b : A} {f : a $-> b} {a' : DA a} {b' : DA b},
DHom f a' b' → DHom (fmap F f) (F' a a') (F' b b').
Arguments dfmap {A B DA _ _ DB _ _} F {_} F' {_ _ _ _ _ _} f'.
Class IsD2Graph {A : Type} `{Is2Graph A}
(D : A → Type) `{!IsDGraph D}
:= isdgraph_hom : ∀ {a b} {a'} {b'},
IsDGraph (fun (f:a $-> b) ⇒ DHom f a' b').
Global Existing Instance isdgraph_hom.
#[global] Typeclasses Transparent IsD2Graph.
Class IsD1Cat {A : Type} `{Is1Cat A}
(D : A → Type) `{!IsDGraph D, !IsD2Graph D, !IsD01Cat D} :=
{
isd01cat_hom : ∀ {a b : A} {a' : D a} {b' : D b},
IsD01Cat (fun f ⇒ DHom f a' b');
isd0gpd_hom : ∀ {a b : A} {a' : D a} {b' : D b},
IsD0Gpd (fun f ⇒ DHom f a' b');
isd0functor_postcomp : ∀ {a b c : A} {g : b $-> c} {a' : D a}
{b' : D b} {c' : D c} (g' : DHom g b' c'),
@IsD0Functor _ _ (fun f ⇒ DHom f a' b')
_ _ (fun gf ⇒ DHom gf a' c')
_ _ (cat_postcomp a g) _ (dcat_postcomp g');
isd0functor_precomp : ∀ {a b c : A} {f : a $-> b} {a' : D a}
{b' : D b} {c' : D c} (f' : DHom f a' b'),
@IsD0Functor _ _ (fun g ⇒ DHom g b' c')
_ _ (fun gf ⇒ DHom gf a' c')
_ _ (cat_precomp c f) _ (dcat_precomp f');
dcat_assoc : ∀ {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
DHom (cat_assoc f g h) ((h' $o' g') $o' f')
(h' $o' (g' $o' f'));
dcat_assoc_opp : ∀ {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
DHom (cat_assoc_opp f g h) (h' $o' (g' $o' f'))
((h' $o' g') $o' f');
dcat_idl : ∀ {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
(f' : DHom f a' b'), DHom (cat_idl f) (DId b' $o' f') f';
dcat_idr : ∀ {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
(f' : DHom f a' b'), DHom (cat_idr f) (f' $o' DId a') f';
}.
Global Existing Instance isd01cat_hom.
Global Existing Instance isd0gpd_hom.
Global Existing Instance isd0functor_postcomp.
Global Existing Instance isd0functor_precomp.
Definition dcat_postwhisker {A : Type} {D : A → Type} `{IsD1Cat A D}
{a b c : A} {f g : a $-> b} {h : b $-> c} {p : f $== g}
{a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'}
(h' : DHom h b' c') (p' : DHom p f' g')
: DHom (h $@L p) (h' $o' f') (h' $o' g')
:= dfmap (cat_postcomp a h) (dcat_postcomp h') p'.
Notation "h $@L' p" := (dcat_postwhisker h p).
Definition dcat_prewhisker {A : Type} {D : A → Type} `{IsD1Cat A D}
{a b c : A} {f : a $-> b} {g h : b $-> c} {p : g $== h}
{a' : D a} {b' : D b} {c' : D c} {g' : DHom g b' c'} {h' : DHom h b' c'}
(p' : DHom p g' h') (f' : DHom f a' b')
: DHom (p $@R f) (g' $o' f') (h' $o' f')
:= dfmap (cat_precomp c f) (dcat_precomp f') p'.
Notation "p $@R' f" := (dcat_prewhisker p f).
Definition dcat_comp2 {A : Type} {D : A → Type} `{IsD1Cat A D} {a b c : A}
{f g : a $-> b} {h k : b $-> c} {p : f $== g} {q : h $== k}
{a' : D a} {b' : D b} {c' : D c} {f' : DHom f a' b'} {g' : DHom g a' b'}
{h' : DHom h b' c'} {k' : DHom k b' c'}
(p' : DHom p f' g') (q' : DHom q h' k')
: DHom (p $@@ q) (h' $o' f') (k' $o' g')
:= (k' $@L' p') $o' (q' $@R' f').
Notation "q $@@' p" := (dcat_comp2 q p).
Monomorphisms and epimorphisms.
Definition DMonic {A} {D : A → Type} `{IsD1Cat A D} {b c : A}
{f : b $-> c} {mon : Monic f} {b' : D b} {c' : D c} (f' : DHom f b' c')
:= ∀ (a : A) (g h : a $-> b) (p : f $o g $== f $o h) (a' : D a)
(g' : DHom g a' b') (h' : DHom h a' b'),
DGpdHom p (f' $o' g') (f' $o' h') → DGpdHom (mon a g h p) g' h'.
Definition DEpic {A} {D : A → Type} `{IsD1Cat A D} {a b : A}
{f : a $-> b} {epi : Epic f} {a' : D a} {b' : D b} (f' : DHom f a' b')
:= ∀ (c : A) (g h : b $-> c) (p : g $o f $== h $o f) (c' : D c)
(g' : DHom g b' c') (h' : DHom h b' c'),
DGpdHom p (g' $o' f') (h' $o' f') → DGpdHom (epi c g h p) g' h'.
Global Instance isgraph_total {A : Type} (D : A → Type) `{IsDGraph A D}
: IsGraph (sig D).
Proof.
srapply Build_IsGraph.
intros [a a'] [b b'].
exact {f : a $-> b & DHom f a' b'}.
Defined.
Global Instance is01cat_total {A : Type} (D : A → Type) `{IsD01Cat A D}
: Is01Cat (sig D).
Proof.
srapply Build_Is01Cat.
- intros [a a'].
exact (Id a; DId a').
- intros [a a'] [b b'] [c c'] [g g'] [f f'].
exact (g $o f; g' $o' f').
Defined.
Global Instance is0gpd_total {A : Type} (D : A → Type) `{IsD0Gpd A D}
: Is0Gpd (sig D).
Proof.
srapply Build_Is0Gpd.
intros [a a'] [b b'] [f f'].
exact (f^$; dgpd_rev f').
Defined.
Global Instance is0functor_total_pr1 {A : Type} (D : A → Type) `{IsDGraph A D}
: Is0Functor (pr1 : sig D → A).
Proof.
srapply Build_Is0Functor.
intros [a a'] [b b'] [f f'].
exact f.
Defined.
Global Instance is2graph_total {A : Type} (D : A → Type) `{IsD2Graph A D}
: Is2Graph (sig D).
Proof.
intros [a a'] [b b'].
srapply Build_IsGraph.
intros [f f'] [g g'].
exact ({p : f $-> g & DHom p f' g'}).
Defined.
Global Instance is0functor_total {A : Type} (DA : A → Type) `{IsD01Cat A DA}
{B : Type} (DB : B → Type) `{IsD01Cat B DB} (F : A → B) `{!Is0Functor F}
(F' : ∀ (a : A), DA a → DB (F a)) `{!IsD0Functor F F'}
: Is0Functor (functor_sigma F F').
Proof.
srapply Build_Is0Functor.
intros [a a'] [b b'].
intros [f f'].
exact (fmap F f; dfmap F F' f').
Defined.
Global Instance is1cat_total {A : Type} (D : A → Type) `{IsD1Cat A D}
: Is1Cat (sig D).
Proof.
srapply Build_Is1Cat.
- intros [a a'] [b b'] [c c'] [f f'].
apply Build_Is0Functor.
intros [g g'] [h h'] [p p'].
exact (f $@L p; f' $@L' p').
- intros [a a'] [b b'] [c c'] [f f'].
apply Build_Is0Functor.
intros [g g'] [h h'] [p p'].
exact (p $@R f; p' $@R' f').
- intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].
exact (cat_assoc f g h; dcat_assoc f' g' h').
- intros [a a'] [b b'] [c c'] [d d'] [f f'] [g g'] [h h'].
exact (cat_assoc_opp f g h; dcat_assoc_opp f' g' h').
- intros [a a'] [b b'] [f f'].
exact (cat_idl f; dcat_idl f').
- intros [a a'] [b b'] [f f'].
exact (cat_idr f; dcat_idr f').
Defined.
Global Instance is1functor_pr1 {A : Type} {D : A → Type} `{IsD1Cat A D}
: Is1Functor (pr1 : sig D → A).
Proof.
srapply Build_Is1Functor.
- intros [a a'] [b b'] [f f'] [g g'] [p p'].
exact p.
- intros [a a'].
apply Id.
- intros [a a'] [b b'] [c c'] [f f'] [g g'].
apply Id.
Defined.
Class IsD1Cat_Strong {A : Type} `{Is1Cat_Strong A}
(D : A → Type)
`{!IsDGraph D, !IsD2Graph D, !IsD01Cat D} :=
{
isd01cat_hom_strong : ∀ {a b : A} {a' : D a} {b' : D b},
IsD01Cat (fun f ⇒ DHom f a' b');
isd0gpd_hom_strong : ∀ {a b : A} {a' : D a} {b' : D b},
IsD0Gpd (fun f ⇒ DHom f a' b');
isd0functor_postcomp_strong : ∀ {a b c : A} {g : b $-> c} {a' : D a}
{b' : D b} {c' : D c} (g' : DHom g b' c'),
@IsD0Functor _ _ (fun f ⇒ DHom f a' b')
_ _ (fun gf ⇒ DHom gf a' c')
_ _ (cat_postcomp a g) _ (dcat_postcomp g');
isd0functor_precomp_strong : ∀ {a b c : A} {f : a $-> b} {a' : D a}
{b' : D b} {c' : D c} (f' : DHom f a' b'),
@IsD0Functor _ _ (fun g ⇒ DHom g b' c')
_ _ (fun gf ⇒ DHom gf a' c')
_ _ (cat_precomp c f) _ (dcat_precomp f');
dcat_assoc_strong : ∀ {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
(transport (fun k ⇒ DHom k a' d') (cat_assoc_strong f g h)
((h' $o' g') $o' f')) = h' $o' (g' $o' f');
dcat_assoc_opp_strong : ∀ {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d}
{a' : D a} {b' : D b} {c' : D c} {d' : D d}
(f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d'),
(transport (fun k ⇒ DHom k a' d') (cat_assoc_opp_strong f g h)
(h' $o' (g' $o' f'))) = (h' $o' g') $o' f';
dcat_idl_strong : ∀ {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
(f' : DHom f a' b'),
(transport (fun k ⇒ DHom k a' b') (cat_idl_strong f)
(DId b' $o' f')) = f';
dcat_idr_strong : ∀ {a b : A} {f : a $-> b} {a' : D a} {b' : D b}
(f' : DHom f a' b'),
(transport (fun k ⇒ DHom k a' b') (cat_idr_strong f)
(f' $o' DId a')) = f';
}.
Global Existing Instance isd01cat_hom_strong.
Global Existing Instance isd0gpd_hom_strong.
Global Existing Instance isd0functor_postcomp_strong.
Global Existing Instance isd0functor_precomp_strong.
(* If in the future we make a Build_Is1Cat_Strong' that lets the user omit the second proof of associativity, this shows how it can be recovered from the original proof:
Definition dcat_assoc_opp_strong {A : Type} {D : A -> Type} `{IsD1Cat_Strong A D}
{a b c d : A} {f : a -> c} {h : c o' (g' o' g') *)
Global Instance isd1cat_isd1catstrong {A : Type} (D : A → Type)
`{IsD1Cat_Strong A D} : IsD1Cat D.
Proof.
srapply Build_IsD1Cat.
- intros a b c d f g h a' b' c' d' f' g' h'.
exact (DHom_path (cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
- intros a b c d f g h a' b' c' d' f' g' h'.
exact (DHom_path (cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
- intros a b f a' b' f'.
exact (DHom_path (cat_idl_strong f) (dcat_idl_strong f')).
- intros a b f a' b' f'.
exact (DHom_path (cat_idr_strong f) (dcat_idr_strong f')).
Defined.
Global Instance is1catstrong_total {A : Type}
(D : A → Type) `{IsD1Cat_Strong A D}
: Is1Cat_Strong (sig D).
Proof.
srapply Build_Is1Cat_Strong.
- intros aa' bb' cc' dd' [f f'] [g g'] [h h'].
exact (path_sigma' _
(cat_assoc_strong f g h) (dcat_assoc_strong f' g' h')).
- intros aa' bb' cc' dd' [f f'] [g g'] [h h'].
exact (path_sigma' _
(cat_assoc_opp_strong f g h) (dcat_assoc_opp_strong f' g' h')).
- intros aa' bb' [f f'].
exact (path_sigma' _ (cat_idl_strong f) (dcat_idl_strong f')).
- intros aa' bb' [f f'].
exact (path_sigma' _ (cat_idr_strong f) (dcat_idr_strong f')).
Defined.
Class IsD1Functor
{A B : Type} {DA : A → Type} `{IsD1Cat A DA} {DB : B → Type} `{IsD1Cat B DB}
(F : A → B) `{!Is0Functor F, !Is1Functor F}
(F' : ∀ (a : A), DA a → DB (F a)) `{!IsD0Functor F F'} :=
{
dfmap2 : ∀ {a b : A} {f g : a $-> b} {p : f $== g} {a' : DA a}
{b' : DA b} (f' : DHom f a' b') (g' : DHom g a' b'),
DHom p f' g' → DHom (fmap2 F p) (dfmap F F' f') (dfmap F F' g');
dfmap_id : ∀ {a : A} (a' : DA a),
DHom (fmap_id F a) (dfmap F F' (DId a')) (DId (F' a a'));
dfmap_comp : ∀ {a b c : A} {f : a $-> b} {g : b $-> c} {a' : DA a}
{b' : DA b} {c' : DA c} (f' : DHom f a' b') (g' : DHom g b' c'),
DHom (fmap_comp F f g) (dfmap F F' (g' $o' f'))
(dfmap F F' g' $o' dfmap F F' f');
}.
Arguments dfmap2 {A B DA _ _ _ _ _ _ _ _ DB _ _ _ _ _ _ _ _}
F {_ _} F' {_ _ a b f g p a' b' f' g'} p'.
Arguments dfmap_id {A B DA _ _ _ _ _ _ _ _ DB _ _ _ _ _ _ _ _}
F {_ _} F' {_ _ a} a'.
Arguments dfmap_comp {A B DA _ _ _ _ _ _ _ _ DB _ _ _ _ _ _ _ _}
F {_ _} F' {_ _ a b c f g a' b' c'} f' g'.
Global Instance is1functor_total {A B : Type} (DA : A → Type) (DB : B → Type)
(F : A → B) (F' : ∀ (a : A), DA a → DB (F a)) `{IsD1Functor A B DA DB F F'}
: Is1Functor (functor_sigma F F').
Proof.
srapply Build_Is1Functor.
- intros [a a'] [b b'] [f f'] [g g'] [p p'].
∃ (fmap2 F p).
exact (dfmap2 F F' p').
- intros [a a'].
exact (fmap_id F a; dfmap_id F F' a').
- intros [a a'] [b b'] [c c'] [f f'] [g g'].
exact (fmap_comp F f g; dfmap_comp F F' f' g').
Defined.
Section IdentityFunctor.
Global Instance isd0functor_idmap {A : Type} `{Is01Cat A}
(DA : A → Type) `{!IsDGraph DA, !IsD01Cat DA}
: IsD0Functor (idmap) (fun a a' ⇒ a').
Proof.
intros a b f a' b' f'.
assumption.
Defined.
Global Instance isd1functor_idmap {A : Type} (DA : A → Type)
`{IsD1Cat A DA}
: IsD1Functor (idmap) (fun a a' ⇒ a').
Proof.
apply Build_IsD1Functor.
- intros a b f g p a' b' f' g' p'.
assumption.
- intros a a'.
apply DId.
- intros a b c f g a' b' c' f' g'.
apply DId.
Defined.
End IdentityFunctor.
Section ConstantFunctor.
Global Instance isd0functor_const {A : Type} `{IsGraph A}
{B : Type} `{Is01Cat B} (DA : A → Type) `{!IsDGraph DA}
(DB : B → Type) `{!IsDGraph DB, !IsD01Cat DB} (x : B) (x' : DB x)
: IsD0Functor (fun _ : A ⇒ x) (fun _ _ ⇒ x').
Proof.
intros a b f a' b' f'.
apply DId.
Defined.
Global Instance isd1functor_const {A : Type} {B : Type}
(DA : A → Type)
`{IsD1Cat A DA}
(DB : B → Type)
`{IsD1Cat B DB}
(x : B) (x' : DB x)
: IsD1Functor (fun _ ⇒ x) (fun _ _ ⇒ x').
Proof.
snrapply Build_IsD1Functor.
- intros a b f g p a' b' f' g' p'.
apply DId.
- intros a a'.
apply DId.
- intros a b c f g a' b' c' f' g'.
apply dgpd_rev.
apply dcat_idl.
Defined.
End ConstantFunctor.
Section CompositeFunctor.
Context {A B C : Type} {DA : A → Type} {DB : B → Type} {DC : C → Type}
(F : A → B) (G : B → C)
(F' : ∀ (a : A), DA a → DB (F a))
(G' : ∀ (b : B), DB b → DC (G b)).
Global Instance isd0functor_compose
`{IsDGraph A DA} `{IsDGraph B DB} `{IsDGraph C DC}
`{!Is0Functor F} `{!Is0Functor G}
`{!IsD0Functor F F'} `{!IsD0Functor G G'}
: IsD0Functor (G o F) (fun a a' ⇒ (G' (F a) o (F' a)) a').
Proof.
intros a b f a' b' f'.
exact (dfmap G G' (dfmap F F' f')).
Defined.
Global Instance isd1functor_compose
`{IsD1Cat A DA} `{IsD1Cat B DB} `{IsD1Cat C DC}
`{!Is0Functor F, !Is1Functor F} `{!Is0Functor G, !Is1Functor G}
`{!IsD0Functor F F', !IsD1Functor F F'}
`{!IsD0Functor G G', !IsD1Functor G G'}
: IsD1Functor (G o F) (fun a a' ⇒ (G' (F a) o (F' a)) a').
Proof.
snrapply Build_IsD1Functor.
- intros a b f g p a' b' f' g' p'.
apply (dfmap2 _ _ (dfmap2 F F' p')).
- intros a a'.
apply (dfmap2 _ _ (dfmap_id F F' a') $@' dfmap_id G G' _).
- intros a b c f g a' b' c' f' g'.
apply (dfmap2 _ _ (dfmap_comp F F' f' g') $@' dfmap_comp G G' _ _).
Defined.
End CompositeFunctor.
Local Definition pointwise_prod {A B : Type} (DA : A → Type) (DB : B → Type)
(x : A × B) := DA (fst x) × DB (snd x).
Global Instance isdgraph_prod {A B : Type} (DA : A → Type) `{IsDGraph A DA}
(DB : B → Type) `{IsDGraph B DB}
: IsDGraph (pointwise_prod DA DB).
Proof.
intros [a1 b1] [a2 b2] [f g] [a1' b1'] [a2' b2'].
exact (DHom f a1' a2' × DHom g b1' b2').
Defined.
Global Instance isd01cat_prod {A B : Type} (DA : A → Type) `{IsD01Cat A DA}
(DB : B → Type) `{IsD01Cat B DB}
: IsD01Cat (pointwise_prod DA DB).
Proof.
srapply Build_IsD01Cat.
- intros [a b] [a' b'].
exact (DId a', DId b').
- intros [a1 b1] [a2 b2] [a3 b3] [f2 g2] [f1 g1] [a1' b1'] [a2' b2'] [a3' b3'].
intros [f2' g2'] [f1' g1'].
exact (f2' $o' f1', g2' $o' g1').
Defined.
Global Instance isd0gpd_prod {A B : Type} (DA : A → Type) `{IsD0Gpd A DA}
(DB : B → Type) `{IsD0Gpd B DB}
: IsD0Gpd (pointwise_prod DA DB).
Proof.
intros [a1 b1] [a2 b2] [f g] [a1' b1'] [a2' b2'] [f' g'].
exact (f'^$', g'^$').
Defined.
Global Instance isd2graph_prod {A B : Type} (DA : A → Type) `{IsD2Graph A DA}
(DB : B → Type) `{IsD2Graph B DB}
: IsD2Graph (pointwise_prod DA DB).
Proof.
intros [a1 b1] [a2 b2] [a1' b1'] [a2' b2'].
srapply isdgraph_prod.
Defined.
Global Instance isd1cat_prod {A B : Type} (DA : A → Type) `{IsD1Cat A DA}
(DB : B → Type) `{IsD1Cat B DB}
: IsD1Cat (pointwise_prod DA DB).
Proof.
snrapply Build_IsD1Cat.
- intros ab1 ab2 ab1' ab2'.
srapply isd01cat_prod.
- intros ab1 ab2 ab1' ab2'.
srapply (isd0gpd_prod _ _).
- intros ab1 ab2 ab3 fg ab1' ab2' ab3' [f' g'].
intros hk1 hk2 pq hk1' hk2' [p' q'].
exact (f' $@L' p', g' $@L' q').
- intros ab1 ab2 ab3 fg ab1' ab2' ab3' [f' g'].
intros hk1 hk2 pq hk1' hk2' [p' q'].
exact (p' $@R' f', q' $@R' g').
- intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.
intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].
exact (dcat_assoc f1' f2' f3', dcat_assoc g1' g2' g3').
- intros ab1 ab2 ab3 ab4 fg1 fg2 fg3.
intros ab1' ab2' ab3' ab4' [f1' g1'] [f2' g2'] [f3' g3'].
exact (dcat_assoc_opp f1' f2' f3', dcat_assoc_opp g1' g2' g3').
- intros ab1 ab2 fg ab1' ab2' [f' g'].
exact (dcat_idl f', dcat_idl g').
- intros ab1 ab2 fg ab1' ab2' [f' g'].
exact (dcat_idr f', dcat_idr g').
Defined.