(* -*- mode: coq; mode: visual-line -*-  *)

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 Global Instances because we only want to apply them manually, but we make them Local Instances 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
    nrapply 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
    nrapply 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 apply 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
    nrapply 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
    apply 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
    nrapply 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
    snrapply 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) nrapply 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) rapply 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 rapply 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 rapply 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 rapply 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
    constructor.
A, B: Type
f: A -> B
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
H0: HasMorExt B
forall (a b : A) (f g : a $-> b), IsEquiv GpdHom_path intros_of_type A; 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 apply 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 nrapply 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) nrapply 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) nrapply 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 nrapply catie_adjointify'.
  Defined.

End Induced_category.