Library TypeTheory.OtherDefs.CwF_Pitts_to_TypeCat
- Construction of a type-precategory from a precategory with Families
- Proof that the constructed type-precategory is split
Require Import UniMath.CategoryTheory.total2_paths.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import TypeTheory.Auxiliary.UnicodeNotations.
Require Import TypeTheory.ALV1.TypeCat.
Require Import TypeTheory.OtherDefs.CwF_Pitts.
Require Import TypeTheory.Auxiliary.Auxiliary.
Set Automatic Introduction.
Local Notation "γ ## a" := (pairing γ a) (at level 75).
Section Prelims.
Definition pairing_transport {CC : precategory} (C : cwf_struct CC) {Γ} {A A' : C⟨Γ⟩} (e : A = A')
{Γ'} (γ : Γ' --> Γ) (a : C ⟨Γ'⊢A{{γ}}⟩)
: (γ ## a) ;; idtoiso (maponpaths (fun (B : C⟨Γ⟩) => Γ∙B) e)
= (γ ## (transportf (fun B => C ⟨ Γ' ⊢ B {{γ}}⟩) e a)).
Proof.
destruct e; simpl.
apply id_right.
Defined.
Lemma transportf_maponpaths {CC : precategory} {C : cwf_struct CC} {Γ} {B B' : C⟨Γ⟩} (e : B = B')
{Γ'} (f : Γ' --> Γ) (b : C ⟨ Γ' ⊢ B{{f}} ⟩)
: transportf (term C Γ') (maponpaths (fun D => D{{f}}) e) b
= transportf (fun D => term C Γ' (D{{f}})) e b.
Proof.
apply pathsinv0.
apply (@functtransportf _ _ (λ D : C ⟨Γ⟩, D {{f}})).
Defined.
End Prelims.
Type-precat from precat with Families
Section TypePreCat_of_PreCwF.
Context (CC : precategory) (C : cwf_struct CC) (homs_sets : has_homsets CC).
Definition type_cat1_of_precwf : typecat_structure1 CC.
Proof.
unfold typecat_structure1.
exists (type C).
exists (comp_obj ).
exact (fun Γ a Γ' f => a{{f}}).
Defined.
We can now assemble the components into a type-precategory:
Definition type_cat_of_precwf : typecat_structure CC.
Proof.
exists type_cat1_of_precwf.
unfold typecat_structure2.
exists (@proj_mor CC C).
exists (@q_precwf CC C).
exists (@dpr_q_precwf CC C).
intros; apply @is_symmetric_isPullback. { apply homs_sets. }
apply is_pullback_reindx_cwf. apply homs_sets.
Defined.
Definition issplit_type_precat_of_precwf
: is_split_typecat type_cat_of_precwf.
Proof.
unfold is_split_typecat.
repeat split.
-
apply cwf_types_isaset.
-
exists (reindx_type_id C).
intros Γ A.
unfold q_typecat; simpl. unfold q_precwf.
eapply pathscomp0. Focus 2. apply id_left.
eapply pathscomp0. Focus 2.
refine (maponpaths (fun q => q ;; _) _).
Unfocus.
eapply pathscomp0. Focus 2.
symmetry. apply pairing_transport.
Focus 2. apply cwf_law_4.
eapply pathscomp0.
apply (pairing_mapeq _ _ (id_right _ )).
apply maponpaths. simpl.
eapply pathscomp0. apply transport_f_f.
unshelve refine (_ @ _).
exact (transportf (term C (Γ ◂ reind_typecat A (identity Γ)))
(maponpaths (fun B => B {{π (A {{identity Γ}})}}) (reindx_type_id C Γ A))
(ν (A {{identity Γ}}))).
apply term_typeeq_transport_lemma.
apply term_typeeq_transport_lemma_2.
reflexivity.
apply transportf_maponpaths.
-
exists (fun Γ A Γ' f Γ'' g => reindx_type_comp C f g A).
intros Γ A Γ' f Γ'' g.
unfold q_typecat. simpl.
match goal with [|- _ = ?e ] =>
pathvia (identity _ ;; e); [| apply id_left] end.
rewrite assoc.
rewrite assoc.
unfold ext_typecat. simpl.
rewrite <- cwf_law_4.
rewrite pairing_transport.
unfold q_precwf.
rewrite cwf_law_3.
match goal with [|- pairing ?b _ = pairing ?e _ ] =>
set (X := b); set (X' := e) end.
etrans.
+ refine (pairing_mapeq _ X' _ _ ).
unfold X; clear X; unfold X'; clear X'.
etrans. Focus 2. eapply pathsinv0.
cancel_postcomposition. apply cwf_law_3.
etrans. Focus 2. eapply pathsinv0. apply assoc.
etrans. apply assoc.
cancel_postcomposition.
etrans. Focus 2. eapply pathsinv0. apply cwf_law_1.
etrans; [ | eapply pathsinv0; apply assoc ].
cancel_postcomposition. sym. apply cwf_law_1.
+ apply maponpaths.
match goal with |[ |- transportf _ ?e _ = transportf _ ?e' _ ] =>
generalize e; generalize e' end.
intros p p'.
rew_trans_@.
apply term_typeeq_transport_lemma.
etrans. Focus 2.
apply rterm_typeeq.
match goal with |[ |- transportf _ ?e _ = transportf _ ?e' _ ] =>
generalize e; generalize e' end.
clear p p'.
intros p p'.
clear X'.
rewrite (reindx_term_comp C).
rewrite transport_f_f.
match goal with |[ |- transportf _ ?e _ = transportf _ ?e' _ ] =>
generalize e' end.
clear p.
intro p.
rewrite pre_cwf_law_2'.
unfold transportb.
rewrite transport_f_f.
rewrite transport_f_f.
apply term_typeeq_transport_lemma.
match goal with |[ |- _ = transportf _ ?e _ ⟦ _ ⟧ ] => generalize e end.
intro q.
etrans. Focus 2. apply rterm_typeeq.
rewrite pre_cwf_law_2'.
rewrite transport_f_f.
unfold transportb.
rewrite transport_f_f.
match goal with |[ |- transportf _ ?e _ = transportf _ ?e' _ ] =>
generalize e; generalize e' end.
intros P P'. clear p q. clear p'.
match goal with |[ |- _ = transportf _ _ (transportf _ ?e' _ ) ] =>
set (Q:=e') end.
apply term_typeeq_transport_lemma.
match goal with |[ |- transportf _ ?e _ = transportf _ ?e' _ ] =>
generalize e end.
intro p.
clear P P'.
clear X.
assert (X : p = maponpaths (fun x => x {{π (A {{g ;; f}})}}) Q).
{ apply cwf_types_isaset. }
rewrite X.
apply pathsinv0. apply retype_term_pi.
Qed.
End TypePreCat_of_PreCwF.