Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(* -*- mode: coq; mode: visual-line -*- *)
[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. *)Ltacintros_of_type A :=
repeatmatch goal with |- forall (a : A), _ => intro a end.SectionInduced_category.Context {AB : Type} (f : A -> B).
A, B: Type f: A -> B H: IsGraph B
IsGraph A
A, B: Type f: A -> B H: IsGraph B
IsGraph A
A, B: Type f: A -> B H: IsGraph B
A -> A -> Type
A, B: Type f: A -> B H: IsGraph B a1, a2: A
Type
exact (f a1 $-> f a2).Defined.
A, B: Type f: A -> B H: IsGraph B H0: Is01Cat B
Is01Cat A
A, B: Type f: A -> B H: IsGraph B H0: Is01Cat B
Is01Cat A
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.
A, B: Type f: A -> B H: IsGraph B H0: Is01Cat B H1: Is0Gpd B
Is0Gpd A
A, B: Type f: A -> B H: IsGraph B H0: Is01Cat B H1: Is0Gpd B
Is0Gpd A
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. *)
A, B: Type f: A -> B H: IsGraph B
Is0Functor f
A, B: Type f: A -> B H: IsGraph B
Is0Functor f
A, B: Type f: A -> B H: IsGraph B a, b: A
(f a $-> f b) -> f a $-> f b
exact idmap.Defined.
A, B: Type f: A -> B H: IsGraph B H0: Is2Graph B
Is2Graph A
A, B: Type f: A -> B H: IsGraph B H0: Is2Graph B
Is2Graph A
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.
A, B: Type f: A -> B IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B
Is1Cat A
A, B: Type f: A -> B IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B
Is1Cat A
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
forallg : 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
forallf0 : 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
forallf0 : 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
forallf0 : 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
forallg : 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
forallf0 : 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
forallf0 : 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
forallf0 : f a $-> f b, f0 $o Id (f a) $-> f0
rapply cat_idr.Defined.
A, B: Type f: A -> B IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B
Is1Functor f
A, B: Type f: A -> B IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B
Is1Functor f
A, B: Type f: A -> B IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B a, b: A
forallf0g : 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
forallf0g : 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, 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
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.
A, B: Type f: A -> B IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B H0: 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
A, B: Type f: A -> B IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B H0: HasMorExt B
forall (ab : A) (fg : a $-> b), IsEquiv GpdHom_path
A, B: Type f: A -> B IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B H0: HasMorExt B a, b: A
forallf0g : f a $-> f b, IsEquiv GpdHom_path
rapply isequiv_Htpy_path.Defined.
A, B: Type f: A -> B IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B H0: 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
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
forallf0 : ?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
forallf0 : 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
forallf0 : ?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
forallf0 : ?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
forallf0 : 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
forallf0 : 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
forallf0 : 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
forallf0 : 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