Merge pull request #189 from tvignon/types_structure_over_cwf

Sigma, Pi and Identity Types structure over cwf

Author: benediktahrens

TypeTheory/TypeConstructions/.package/files

@@ -1 +1,2 @@
-CwF_SplitTypeCat_TypeEquiv.v
+CwF_Structure_Display.v
+CwF_SplitTypeCat_TypeEquiv.v

TypeTheory/TypeConstructions/CwF_SplitTypeCat_TypeEquiv.v

@@ -33,7 +33,7 @@ Local Definition Tm : functor _ _ := source pp.
 Local Definition ext {Γ : C} (A : Ty Γ : hSet) : C := pr11(pr22 CwF Γ A).
 Local Notation "Γ.: A" :=  (ext A) (at level 24).
 
-Definition pi {Γ :C} (A : Ty Γ : hSet) : C⟦Γ.:A,Γ⟧ := pr21 (pr22 CwF _ A).
+Local Definition pi {Γ :C} (A : Ty Γ : hSet) : C⟦Γ.:A,Γ⟧ := pr21 (pr22 CwF _ A).
 
 (* just a simple to use pp as a nat_trans *)
 Local Definition Nat_trans_morp {C : category} (Γ : C) (p : mor_total(preShv C))