Require Import Basics.Overture Basics.Tactics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.
Require Import WildCat.Equiv.

(** * Induced wild categories *)

(** A map [A -> B] of types, where [B] is some type of wild category, induces the same level of structure on [A], via taking everything to be defined on the image.

This needs to be separate from Core because of [HasEquivs] usage.  We don't make these definitions (exported) [Instance]s because we only want to apply them manually, but we make them [Local Instance]s so that subsequent ones can pick up the previous ones automatically. *)

(** In most of the proofs, we only want to use [intro] on variables of type [A], so this will be handy. *)
Ltac intros_of_type A :=
  repeat match goal with |- forall (a : A), _ => intro a end.

Section Induced_category.
  Context {A B : Type} (f : A -> B).

  Local Instance isgraph_induced `{IsGraph B} : IsGraph A.
A, B: Type
f: A -> B
H: IsGraph B
IsGraph A
  Proof.
A, B: Type
f: A -> B
H: IsGraph B
IsGraph A
    napply Build_IsGraph.
A, B: Type
f: A -> B
H: IsGraph B
A -> A -> Type
    intros a1 a2.
A, B: Type
f: A -> B
H: IsGraph B
a1, a2: A
Type 
    exact (f a1 $-> f a2).
  Defined.

  Local Instance is01cat_induced `{Is01Cat B} : Is01Cat A.
A, B: Type
f: A -> B
H: IsGraph B
H0: Is01Cat B
Is01Cat A
  Proof.
A, B: Type
f: A -> B
H: IsGraph B
H0: Is01Cat B
Is01Cat A
    napply Build_Is01Cat; intros_of_type A; cbn.
A, B: Type
f: A -> B
H: IsGraph B
H0: Is01Cat B
a: A
f a $-> f a
A, B: Type
f: A -> B
H: IsGraph B
H0: Is01Cat B
a, b, c: A
(f b $-> f c) -> (f a $-> f b) -> f a $-> f c
    +
A, B: Type
f: A -> B
H: IsGraph B
H0: Is01Cat B
a: A
f a $-> f a apply Id.
    +
A, B: Type
f: A -> B
H: IsGraph B
H0: Is01Cat B
a, b, c: A
(f b $-> f c) -> (f a $-> f b) -> f a $-> f c exact cat_comp.
  Defined.

  Local Instance is0gpd_induced `{Is0Gpd B} : Is0Gpd A.
A, B: Type
f: A -> B
H: IsGraph B
H0: Is01Cat B
H1: Is0Gpd B
Is0Gpd A
  Proof.
A, B: Type
f: A -> B
H: IsGraph B
H0: Is01Cat B
H1: Is0Gpd B
Is0Gpd A
    napply Build_Is0Gpd; intros_of_type A; cbn.
A, B: Type
f: A -> B
H: IsGraph B
H0: Is01Cat B
H1: Is0Gpd B
a, b: A
(f a $-> f b) -> f b $-> f a
    exact gpd_rev.
  Defined.

  (** The structure map along which we induce the category structure becomes a functor with respect to the induced structure. *)
  Local Instance is0functor_induced `{IsGraph B} : Is0Functor f.
A, B: Type
f: A -> B
H: IsGraph B
Is0Functor f
  Proof.
A, B: Type
f: A -> B
H: IsGraph B
Is0Functor f
    napply Build_Is0Functor; intros_of_type A; cbn.
A, B: Type
f: A -> B
H: IsGraph B
a, b: A
(f a $-> f b) -> f a $-> f b
    exact idmap.
  Defined.

  Local Instance is2graph_induced `{Is2Graph B} : Is2Graph A.
A, B: Type
f: A -> B
H: IsGraph B
H0: Is2Graph B
Is2Graph A
  Proof.
A, B: Type
f: A -> B
H: IsGraph B
H0: Is2Graph B
Is2Graph A
    constructor; cbn.
A, B: Type
f: A -> B
H: IsGraph B
H0: Is2Graph B
a, b: A
(f a $-> f b) -> (f a $-> f b) -> Type apply isgraph_hom.
  Defined.

  Local Instance is1cat_induced `{Is1Cat B} : Is1Cat A.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
Is1Cat A
  Proof.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
Is1Cat A
    snapply Build_Is1Cat; intros_of_type A; cbn.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
Is01Cat (f a $-> f b)
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
Is0Gpd (f a $-> f b)
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c: A
forall g : f b $-> f c, Is0Functor (cat_comp g)
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c: A
forall f0 : f a $-> f b, Is0Functor (cat_precomp c f0)
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c, d: A
forall (f0 : f a $-> f b) 
(g : f b $-> f c) (h : f c $-> f d),
h $o g $o f0 $-> h $o (g $o f0)
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c, d: A
forall (f0 : f a $-> f b) 
(g : f b $-> f c) (h : f c $-> f d),
h $o (g $o f0) $-> h $o g $o f0
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
forall f0 : f a $-> f b, Id (f b) $o f0 $-> f0
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
forall f0 : f a $-> f b, f0 $o Id (f a) $-> f0
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
Is01Cat (f a $-> f b) rapply is01cat_hom.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
Is0Gpd (f a $-> f b) napply is0gpd_hom.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c: A
forall g : f b $-> f c, Is0Functor (cat_comp g) rapply is0functor_postcomp.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c: A
forall f0 : f a $-> f b, Is0Functor (cat_precomp c f0) rapply is0functor_precomp.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c, d: A
forall (f0 : f a $-> f b) (g : f b $-> f c)
(h : f c $-> f d), h $o g $o f0 $-> h $o (g $o f0) exact cat_assoc.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c, d: A
forall (f0 : f a $-> f b) (g : f b $-> f c)
(h : f c $-> f d), h $o (g $o f0) $-> h $o g $o f0 exact cat_assoc_opp.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
forall f0 : f a $-> f b, Id (f b) $o f0 $-> f0 exact cat_idl.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
forall f0 : f a $-> f b, f0 $o Id (f a) $-> f0 exact cat_idr.
  Defined.

  Local Instance is1functor_induced `{Is1Cat B} : Is1Functor f.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
Is1Functor f
  Proof.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
Is1Functor f
    srapply Build_Is1Functor; intros_of_type A; cbn.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
forall f0 g : f a $-> f b, (f0 $-> g) -> f0 $== g
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a: A
Id (f a) $== Id (f a)
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c: A
forall (f0 : f a $-> f b) 
(g : f b $-> f c), g $o f0 $== g $o f0
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
forall f0 g : f a $-> f b, (f0 $-> g) -> f0 $== g intros g h.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b: A
g, h: f a $-> f b
(g $-> h) -> g $== h exact idmap.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a: A
Id (f a) $== Id (f a) exact (Id _).
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c: A
forall (f0 : f a $-> f b) (g : f b $-> f c),
g $o f0 $== g $o f0 intros g h.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
a, b, c: A
g: f a $-> f b
h: f b $-> f c
h $o g $== h $o g exact (Id _).
  Defined.

  Instance hasmorext_induced `{HasMorExt B} : HasMorExt A.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasMorExt B
HasMorExt A
  Proof.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasMorExt B
HasMorExt A
    intros a b; cbn.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasMorExt B
a, b: A
forall f0 g : f a $-> f b, IsEquiv GpdHom_path rapply isequiv_Htpy_path.
  Defined.

  Definition hasequivs_induced `{HasEquivs B} : HasEquivs A.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
HasEquivs A
  Proof.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
HasEquivs A
    srapply Build_HasEquivs; intros a b; cbn.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
Type
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
(f a $-> f b) -> Type
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
?Goal -> f a $-> f b
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall f0 : ?Goal, ?Goal0 (?Goal1 f0)
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall f0 : f a $-> f b, ?Goal0 f0 -> ?Goal
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall (f0 : f a $-> f b) 
(fe : ?Goal0 f0), ?Goal1 (?Goal3 f0 fe) $-> f0
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
?Goal -> f b $-> f a
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall f0 : ?Goal, ?Goal5 f0 $o ?Goal1 f0 $-> Id (f a)
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall f0 : ?Goal, ?Goal1 f0 $o ?Goal5 f0 $-> Id (f b)
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall (f0 : f a $-> f b) 
(g : f b $-> f a),
(f0 $o g $-> Id (f b)) ->
(g $o f0 $-> Id (f a)) -> ?Goal0 f0
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
Type exact (f a $<~> f b).
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
(f a $-> f b) -> Type apply CatIsEquiv'.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
f a $<~> f b -> f a $-> f b exact cate_fun.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall f0 : f a $<~> f b, CatIsEquiv' (f a) (f b) f0 apply cate_isequiv'.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall f0 : f a $-> f b,
CatIsEquiv' (f a) (f b) f0 -> f a $<~> f b apply cate_buildequiv'.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall (f0 : f a $-> f b)
(fe : CatIsEquiv' (f a) (f b) f0),
cate_buildequiv' (f a) (f b) f0 fe $-> f0 napply cate_buildequiv_fun'.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
f a $<~> f b -> f b $-> f a apply cate_inv'.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall f0 : f a $<~> f b,
cate_inv' (f a) (f b) f0 $o f0 $-> Id (f a) napply cate_issect'.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall f0 : f a $<~> f b,
f0 $o cate_inv' (f a) (f b) f0 $-> Id (f b) napply cate_isretr'.
    +
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasEquivs B
a, b: A
forall (f0 : f a $-> f b) (g : f b $-> f a),
(f0 $o g $-> Id (f b)) ->
(g $o f0 $-> Id (f a)) -> CatIsEquiv' (f a) (f b) f0 napply catie_adjointify'.
  Defined.

End Induced_category.