_CoqProject

-R . Sheafification
-arg -type-in-type 
COQC = /Users/kquiri13/Code/Coq/HoTT8.5/HoTT/hoqc
COQTOP = /Users/kquiri13/Code/Coq/HoTT8.5/HoTT/hoqtop
COQDEP = /Users/kquiri13/Code/Coq/HoTT8.5/HoTT/hoqdep

sheaf_induction.v
Limit/Auxiliary.v
Limit/CechNerve.v
Limit/CoEqualizer.v
Limit/Colimit.v
Limit/limit.v
Limit/Colimit_Prod.v
Limit/Colimit_Sigma.v
Limit/Colimit_trunc.v
Limit/limit_trunc.v
Limit/CommutativeSquares.v
Limit/Diagram.v
Limit/KernelPair.v
Limit/MappingTelescope.v
Limit/MyLemmas.v
Limit/MyTacs.v
Limit.v
PathGroupoid_.v
Equivalences_.v
Forall_.v
MyTacs.v
epi_mono.v
modalities.v
nat_lemmas.v
reflective_subuniverse.v
OPaths.v
T.v
T_telescope.v
sheaf_base_case.v
sheaf_def_and_thm.v
Tf_Omono_sep.v
OT.v
OT_Tf.v