Port Functor and Category from HoTT-categories

This is the first import from
https://github.com/JasonGross/HoTT-categories.  It contains most of the
precategory and functor basic constructions.  Next up is natural
transformations, but first I want feedback on these.

I tried to cut down on the use of crazy tactics a bit (and found a nicer
proof in Functor.Equality) as a result.  I tried to conform to the
naming conventions of the HoTT library, but I'm not sure I got the order
right in most cases, and would appreciate all feedback (especially
stylistic and organizational feedback).
Functor.Equality -> Functor.Paths
Rename things mentioning equality in Functor.Paths

It's called paths now, not eq.
Qualify imports

Otherwise, types.Paths will clash with categories.Functor.Paths.  This
is probably good to do even if we end up renaming
categories.Functor.Paths.
Remove some coercions

Mike Shulman would object to them.  It's confusing to use a proof that
something is an epimorphism where you expect an actual epimorphism.
Attempt to make naming more uniform in categories

I've tried to follow the rule that names should be in the order of
directories (so an associativity law in Functor/Composition is names
functor_compose_associativity).  I'm still not sure if this is a good
choice.  It makes for some wonky clashes, e.g., [functor_compose]
(similar to [ap_compose] and [equiv_compose]) is about composition of
functors, but [category_sum_compose] is composition _in_ the category [A
+ B] (called [category_sum]).

If anyone wants to consistency-check me, the list of names in
categories, generated by

  grep -h -o '\(Definition\|Lemma\|Let\|Proposition\|Theorem\|Axiom\|Parameter\|Corollary\|Record\|Class\|Instance\|Structure\) \+[^ \.]\+' theories/categories/*{,/*}.v | grep -v 'Let ' | grep -o '[^ ]\+$' | sort

Build_PreCategory
Category
category_opposite
category_product
category_sum
category_sum_compose
category_sum_identity
category_sum_morphism
concat_left_identity
concat_right_identity
Epimorphism
equiv_path_functor'_sig
equiv_path_functor'_sig_sig
equiv_sig_functor
equiv_sig_isisomorphism
Functor
functor_compose
functor_compose_associativity
functor_compose_associativity_fst
functor_compose_composition_of
functor_compose_identity_of
functor_identity
functor_inl
functor_inr
functor_left_identity
functor_left_identity_fst
functor_opposite
functor_opposite_inv
functor_right_identity
functor_right_identity_fst
functor_sum
functor_sum_swap
identity_unique
idtoiso
idtoiso_comp
idtoiso_comp3
idtoiso_comp3'
idtoiso_comp4
idtoiso_comp4'
idtoiso_comp5
idtoiso_comp5'
idtoiso_functor
idtoiso_inv
idtoiso_of_transport
InitialObject
initial_object_unique
initial_opposite_terminal
inverse_unique
iscategory_precategory_of_category
IsEpimorphism
isepimorphism_compose
isepimorphism_identity
isepimorphism_isisomorphism
isepimorphism_retr
isequiv_path_isomorphic
isinitial_object_initial
IsIsomorphism
isisomorphism_compose
isisomorphism_identity
isisomorphism_inverse
isisomorphism_isomorphic
IsMonomorphism
ismonomorphism_compose
ismonomorphism_identity
ismonomorphism_isisomorphism
ismonomorphism_sect
iso_compose_pp_V
iso_compose_pV
iso_compose_p_Vp
iso_compose_pV_p
iso_compose_Vp
iso_compose_V_pp
iso_functor
iso_inv_pp
iso_inv_pV
iso_inv_Vp
iso_inv_VV
Isomorphic
isomorphic_refl
Isomorphic_sig
isomorphic_sym
isomorphic_trans
iso_moveL_1M
iso_moveL_1V
iso_moveL_M1
iso_moveL_Mp
iso_moveL_pM
iso_moveL_pV
iso_moveL_V1
iso_moveL_Vp
iso_moveR_1M
iso_moveR_1V
iso_moveR_M1
iso_moveR_Mp
iso_moveR_pM
iso_moveR_pV
iso_moveR_V1
iso_moveR_Vp
isretr_isisomorphism
IsSectionOf
issect_isisomorphism
isstrict_category_product
isstrict_StrictCategory
isterminal_object_terminal
Monomorphism
op_op_functor_id
op_op_id
path_functor
path_functor'
path_functor'_sig
path_functor'_sig_fst
path_functor'_sig_idpath
path_functor'_sig_inv
path_isomorphic
PreCategory
reflexive_epimorphism
reflexive_monomorphism
StrictCategory
sum_swap_swap_id
sum_swap_swap_id_helper
TerminalObject
terminal_object_unique
terminal_opposite_initial
transitive_epimorphism
transitive_monomorphism
Trunc
trunc_category
trunc_functor
trunc_isisomorphism
trunc_Isomorphic
trunc_morphism
unique_up_to_unique_isomorphism

The list of names in HoTT proper, generated by

  grep -h -o '\(Definition\|Lemma\|Let\|Proposition\|Theorem\|Axiom\|Parameter\|Corollary\|Record\|Class\|Instance\|Structure\) \+[^ \.]\+' theories/*{,/*{,/*}}.v | grep -v 'Let ' | grep -o '[^ ]\+$' | sort

is

allpath_extension_conn_map
allpath_hprop
alpha
andb
ap
ap02
ap02_p2p
ap02_pp
ap_1
ap10
ap10_1
ap10_dpath_arrow
ap10_path_arrow
ap10_pp
ap10_V
ap11
ap1_to_conjp
ap_ap10
ap_apply_Fl
ap_apply_FlFr
ap_apply_Fr
ap_apply_l
ap_compose
ap_compose'
ap_const
apD
apD02
apD02_pp
apD10
apD10_1
apD10_path_forall
apD10_pp
apD10_V
apD_const
ap_existT
ap_fst_path_prod
ap_functor_arrow
ap_functor_forall
ap_functor_prod
ap_functor_sigma
ap_idmap
ap_lambda
ap_lambdaD
ap_pp
ap_p_pp
ap_pp_p
ap_sigT_rectnd_path_sigma
ap_snd_path_prod
ap_to_conjp
ap_transport
ap_V
Arrow
atmost
atmost1
atmost1P
axiomK
axiomK_decidable
axiomK_hset
axiomK_idpath
axiomK_isprop
base_path
biimp_path
BiInv
cancelL
cancelL_equiv
cancelL_isequiv
cancelR
cancelR_equiv
cancelR_isequiv
classes_eq_related
class_of_repr
compose
concat
concat_1p
concat2
concat2_1p
concat2_p1
concat_A1p
concat_A1_pp
concat_Ap
concat_A_pp
concat_AT
concat_concat2
concat_p1
concat_pA1
concat_p_A1p
concat_pA1_p
concat_pA1_pp
concat_pA_p
concat_pA_pp
concat_pp_A1
concat_pp_A1p
concat_p_pp
concat_pp_p
concat_pp_V
concat_pV
concat_p_Vp
concat_pV_p
concat_Vp
concat_V_pp
concat_whisker
conj_canV
conjp
conjp_ap
conjp_ap_cancel
conjp_concat
conn_map_comp
conn_map_elim
conn_map_from_extension_elim
conn_pointed_type
conn_point_incl
contr_arrow
contr_basedhtpy
contr_basedpaths
contr_basedpaths'
contr_contr
contr_equiv
contr_equiv'
contr_equiv_contr_contr
contr_equiv_unit
contr_foo
contr_foo
contr_forall
contr_from_Empty
contr_inhabited_hprop
Contr_internal
contr_interval
contr_paths_contr
contr_prod
contr_retr_equiv
contr_sect_equiv
contr_trunc_minus_two
contr_unit
corresponding
decidable_paths
decidable_paths_bool
default_HProp:=
default_HSet:=
dpath_arrow
dpath_forall
dpath_forall'
dpath_path_FFlr
dpath_path_Fl
dpath_path_FlFr
dpath_path_Fr
dpath_path_l
dpath_path_lFFr
dpath_path_lr
dpath_path_r
eckmann_hilton
eisretr_path_sum
eissect_path_sum
epi
epi_mono_equiv
epi_surj
Equiv
equiv_adjointify
equiv_ap
equiv_ap_l
equiv_biinv
equiv_biinv_equiv
equiv_bool_forall_prod
equiv_comp
equiv_compose
equiv_compose'
equiv_composeR'
equiv_concat_l
equiv_concat_lr
equiv_concat_r
equiv_contr_contr
equiv_contr_inhabited_allpath
equiv_contr_inhabited_hprop
equiv_contr_unit
equiv_fcontr_isequiv
equiv_fibration_replacement
equiv_flattening
equiv_flip
equiv_functor_arrow
equiv_functor_arrow'
equiv_functor_forall
equiv_functor_forall'
equiv_functor_forall_id
equiv_functor_prod
equiv_functor_prod'
equiv_functor_prod_l
equiv_functor_prod_r
equiv_functor_sigma
equiv_functor_sigma'
equiv_functor_sigma_id
equiv_functor_sum
equiv_functor_sum'
equiv_functor_sum_l
equiv_functor_sum_r
equiv_homotopic
equiv_hprop_allpath
equiv_hprop_inhabited_contr
equiv_hset_axiomK
equiv_idmap
equiv_iff_hprop
equiv_induction
equiv_inj
equiv_inverse
equiv_isequiv
equiv_loopS1_int
equiv_moveL_pM
equiv_moveR_Vp
equiv_path
equiv_path_arrow
equiv_path_equiv
equiv_path_forall
equiv_path_inverse
equiv_path_prod
equiv_path_sigma
equiv_path_sigma_hprop
equiv_paths_rect
equiv_path_sum
equiv_path_trunctype
equiv_path_unit
equiv_path_universe
equiv_path_V
equiv_postcompose
equiv_postcompose'
equiv_precompose
equiv_precompose'
equiv_prod_corect
equiv_prod_rect
equiv_prod_symm
equiv_rect
equiv_rect
equiv_sigma_assoc
equiv_sigma_contr
equiv_sigma_prod
equiv_sigT_corect
equiv_sigT_rect
equiv_sum_distributive
equiv_sum_rect
equiv_sum_symm
equiv_total_paths
equiv_transport
equiv_uncurry
equiv_unit_corect
eta
eta_1
eta_2
eta2_sigma
eta3_sigma
eta_natural
eta_path_arrow
eta_path_forall
eta_path_prod
eta_path_sigma
eta_path_sigma_uncurried
eta_path_unit
eta_path_universe
eta_prod
eta_sigma
eta_sum
eta_unit
exp
exp'
ExtensionAlong
extension_conn_map_elim
f2p:
False_hp:hProp:=(hp
false_ne_true
Fam
FamequivPow
fcontr_isequiv
fiber_path
fibration_replacement
flip
fmap_agrees_with_univalence
functor_arrow
functor_forall
Functorish
functor_prod
functor_sigma
functor_sum
functor_Truncation
functor_Truncation_idmap
Funext
funext_axiom
funext_axiom
funext_from_interval
Funext_implies_NaiveFunext
hexists
hexists
hfiber
hfiber_fibration
hfiber_triangle
hProp
hprop_allpath
hprop_contr
hprop_Empty
HProp_HProp
hprop_inhabited_contr
hprop_isequiv
hProp_is_hSet
hprop_trunc
hSet
hset_axiomK
hset_decidable
hset_int
hset_sum
htpy_rect
htpy_rect_beta
hunique
implb
in_class
in_class_is_prop
in_class_pr
inhab_prop_contr
inl_injective
interval_rect
interval_rect_beta_seg
interval_rectnd
interval_rectnd_beta_seg
inverse
inverse2
inverse_ap
inv_pp
inv_pV
inv_V
inv_Vp
inv_VV
iota
IsConnected
isconnected_from_iscontr_truncation
IsConnMap
isconn_wedge_incl
iscontr_truncation_from_isconnected
is_epi
IsEquiv
isequiv_adjointify
isequiv_ap
isequiv_cancelL
isequiv_cancelR
isequiv_compose
isequiv_compose'
isequiv_concat_l
isequiv_concat_lr
isequiv_concat_r
isequiv_fcontr
isequiv_flip
isequiv_fmap
isequiv_functor_arrow
isequiv_functor_forall
isequiv_functor_prod
isequiv_functor_sigma
isequiv_functor_sum
isequiv_functor_Truncation
isequiv_homotopic
isequiv_idmap
isequiv_inverse
IsEquivmin1
isequiv_moveL_1M
isequiv_moveL_1V
isequiv_moveL_M1
isequiv_moveL_Mp
isequiv_moveL_pM
isequiv_moveL_pV
isequiv_moveL_transport_p
isequiv_moveL_transport_V
isequiv_moveL_V1
isequiv_moveL_Vp
isequiv_moveR_1M
isequiv_moveR_1V
isequiv_moveR_M1
isequiv_moveR_Mp
isequiv_moveR_pM
isequiv_moveR_pV
isequiv_moveR_transport_p
isequiv_moveR_transport_V
isequiv_moveR_V1
isequiv_moveR_Vp
isequiv_path
isequiv_path_arrow
isequiv_path_equiv
isequiv_path_extension
isequiv_path_forall
isequiv_path_inverse
isequiv_path_prod
isequiv_path_sigma
isequiv_paths_rect
isequiv_path_sum
isequiv_path_unit
isequiv_path_universe
isequiv_postcompose
isequiv_precompose
isequiv_prod_corect
isequiv_prod_rect
isequiv_sigT_corect
isequiv_sigT_of_sum
isequiv_sigT_rect
isequiv_Sph0_to_Bool
isequiv_Sph1_to_S1
isequiv_succ_int
isequiv_sum_of_sigT
isequiv_sum_rect
isequiv_transport
isequiv_unit_corect
isequiv_unit_rect
is_mono
isp
isprop_biinv
iss
issig_contr
issig_equiv
issig_hProp:
issig_isequiv
issig_trunctype
IsTrunc
istrunc_equiv
istrunc_extension_along_conn
istrunc_nullhomotopy
istrunc_paths
istrunc_truncation
istrunc_truncation
istrunc_trunctype
istrunc_trunctype_type
K
left
loop
looptothe
map_twovar
match_eta
match_eta1
match_eta2
merid
min1_path
minus1Trunc_compute_min1
minus1Trunc_compute_min1_nondep
minus1Trunc_compute_path
minus1Trunc_compute_path_nondep
minus1Trunc_ind
minus1Trunc_is_prop
minus1Trunc_map
minus1Trunc_map_compose
minus1Trunc_map_id
minus1Trunc_rect
minus1Trunc_rect_nondep
Misc
moveL_1M
moveL_1V
moveL_E
moveL_M1
moveL_Mp
moveL_pM
moveL_pV
moveL_transport_p
moveL_transport_V
moveL_V1
moveL_Vp
moveR_1M
moveR_1V
moveR_E
moveR_M1
moveR_Mp
moveR_pM
moveR_pV
moveR_transport_p
moveR_transport_V
moveR_V1
moveR_Vp
mu
mu_1
mu_natural
NaiveFunext
NaiveFunext_implies_WeakFunext
negb
neg_injective
neg_neq_pos
neg_neq_zero
not
NullHomotopy
nullhomot_paths_from_susp
nullhomot_susp_from_paths
objclasspb_is_fibrantreplacement
of
of
one_neq_succ_pos
orb
other_adj
p2f:
pack_prod
path2_contr
path_arrow
path_arrow_1
path_biimp
path_contr
path_equiv
path_equiv_biimp
path_equiv_biimp_rec
path_extension
path_forall
path_forall_1
path_forall_1_beta
path_forall2
path_forall_2_beta
path_forall_recr_beta
path_prod
path_prod'
path_prod_uncurried
Paths
path_sigma
path_sigma'
path_sigma_p1_1p'
path_sigma_pp_pp
path_sigma_pp_pp'
path_sigma_uncurried
path_sum
path_sum_inl
path_sum_inr
path_sum_inv
path_trunctype
path_unit
path_unit_uncurried
path_universe
path_universe_uncurried
path_universe_V
path_universe_V_uncurried
pentagon
pointedType:=
pointwise_paths
pos_injective
pos_neq_zero
PowisoFam
pp
ppt
pred_int
prod_corect
prod_corect_uncurried
projT1_path
projT1_path_1
projT1_path_pp
projT1_path_sigma
projT1_path_sigma_uncurried
projT1_path_V
projT2_path
projT2_path_sigma
projT2_path_sigma_uncurried
pullback
quotient_ind
quotient_path2
quotient_rect
quotient_rect_compute
quotient_rect_compute_path
quotient_rect_nondep
quotient_rect_nondep2
quotient_rect_prop
quotient_set
quotient_set
quotient_surjective:
quotient_ump
quotient_ump'
quotient_ump''
Reflexive
reflexive_equiv
reflexive_paths
related_classes_eq
relation
right
S1_code
S1_decode
S1_encode
S1_encode_isequiv
S1_encode_looptothe
S1_rect
S1_rect_beta_loop
S1_rectnd
S1_rectnd_beta_loop
S1_to_Sph1
Sect
seg
set_path2
setrel
sets_exact
sigT_corect
sigT_corect_uncurried
sigT_of_sum
Sn_trunctype:
Sph0_to_Bool
Sph1_to_S1
strength_eta
strength_pentagon_1
strength_pentagon_2
strength_unit
succ_int
succ_pos_injective
sum_of_sigT
sum_rect_uncurried
surj
surj_epi
Susp_comp_merid
Susp_comp_nd_merid
Susp_eta
Susp_eta_homot
Susp_rect
Susp_rect_nd
sWtil_rect
sWtil_rect_beta_cct
sWtil_rect_beta_ppt
sWtil_rectnd
sWtil_rectnd
sWtil_rectnd_beta_ppt
Symmetric
symmetric_equiv
symmetric_paths
t
test
t_natural
topmap
total_path
total_path2
total_path_reconstruction
Transitive
[Transitive]
transitive_equiv
transitive_paths
trans_paths
transport
transport_1
transport2
transport2_const
transport2_is_ap10
transport2_p2p
transport2_V
transport_arrow
transport_compose
transport_const
transportD
transportD_is_transport
transport_exp
transport_forall
transport_forall_constant
transport_path_prod
transport_path_prod'
transport_path_prod'_beta
transport_path_prod'_beta'
transport_path_prod_uncurried
transport_paths_FFlr
transport_paths_Fl
transport_paths_FlFr
transport_paths_FlFr_D
transport_paths_Fr
transport_paths_l
transport_paths_lFFr
transport_paths_lr
transport_paths_r
transport_path_universe
transport_path_universe'
transport_pp
transport_p_pp
transport_prod
transport_pV
transport_pVp
transport_S1_code_loop
transport_S1_code_loopV
transport_sigma
transport_sigma'
transport_sum
transport_Vp
trans_trans_opp2
triangulator
true_ne_false
trunc_arrow
Truncation_rect
Truncation_rect_nondep
trunc_bool
trunc_equiv
trunc_equiv'
trunc_forall
trunc_if
trunc_leq
trunc_prod
trunc_sigma
trunc_succ
trunc_sum
trunc_sum'
TruncType
unique_choice
unit_corect
Unit_hp:hProp:=(hp
Univalence
univalence_axiom
univalence_axiom
unpack_prod
unpack_sigma
WeakFunext
WeakFunext_implies_Funext
wedge_incl_comp1
wedge_incl_comp2
wedge_incl_comp3
wedge_incl_elim
wedge_incl_elim_uncurried
whiskerL
whiskerL_1p
whiskerL_p1
whiskerR
whiskerR_1p
whiskerR_p1
W_rect
W_rect_beta_pp
W_rectnd
W_rectnd_beta_pp
Wtil_rect
Wtil_rect_beta_ppt
Wtil_rectnd
Wtil_rectnd_beta_ppt
Try to use Modules as namespaces

It doesn't quite work, yet; I'm still working on making something like
the following example work:

Module A.
  Parameter x : Type.
End A.

Module B.
  Export A.
End B.

Check B.x.
(* Toplevel input, characters 21-24:
Error: The reference B.x was not found in the current environment. *)
Use [Include] to get constants where we want them.
Merge pull request #219 from JasonGross/categories

Port Functor and Category from HoTT-categories

I looked at how the code changes the rest of the standard library (adds some tactics, changes some details). So it's really an addition to the library, and I think it's ok to add something that may not yet be in perfect condition or super-inspected for all possible details. We should pull it in and work on it.