Merge branch 'type_former_on_SplTCwF' of github.com:tvignon/TypeTheory into type_former_on_SplTCwF

Author: tvignon

TypeTheory/ALV1/CwF_SplitTypeCat_Equivalence.v

@@ -142,7 +142,7 @@ Definition canonical_TM_to_given_iso
   : @iso (preShv C) (tm_from_qq Z) (TM (pr1 Y)).
 Proof.
   exists canonical_TM_to_given.
-  apply functor_iso_if_pointwise_iso.
+  apply functor_iso_if_pointwise_iso. intro c.
   apply canonical_TM_to_given_pointwise_iso.
 Defined.
 

TypeTheory/TypeConstructions/.package/files

@@ -1,2 +1,4 @@
 CwF_SplitTypeCat_TypeEquiv.v
-SplTCwF_TypeFormers.v
+SplTCwF_TypeFormers.v
+CwF_Structure_Display.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))