Library TypeTheory.OtherDefs.CwF_1
- Definition of a precategory with families
- Proof that reindexing forms a pullback
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.category_hset.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import TypeTheory.Auxiliary.Auxiliary.
Require Import TypeTheory.Auxiliary.UnicodeNotations.
Set Automatic Introduction.
Local Notation "# F" := (functor_on_morphisms F)(at level 3).
Module Record_Preview.
Reserved Notation "C ⟨ Γ ⟩" (at level 60).
Reserved Notation "C ⟨ Γ ⊢ A ⟩" (at level 60).
Reserved Notation "A [[ γ ]]" (at level 40).
Reserved Notation "a ⟦ γ ⟧" (at level 40).
Reserved Notation "Γ ∙ A" (at level 35).
Reserved Notation "'π' A" (at level 20).
Reserved Notation "'ν' A" (at level 15).
Reserved Notation "γ ♯ a" (at level 25).
End Record_Preview.
Definition tt_structure (C : precategory) :=
∑ f : functor C^op HSET, ∏ c : C, pr1hSet (f c) → UU.
Definition type {C : precategory} (TT : tt_structure C) : C → hSet := functor_on_objects (pr1 TT).
Notation "C ⟨ Γ ⟩" := (type C Γ) (at level 60).
Definition term {CC : precategory} (C : tt_structure CC) : ∏ Γ : CC, C⟨Γ⟩ → UU := pr2 C.
Notation "C ⟨ Γ ⊢ A ⟩" := (term C Γ A) (at level 60).
Definition rtype {CC : precategory} {C : tt_structure CC}
: ∏ {Γ Γ' : CC} (A : C⟨Γ⟩) (γ : Γ' --> Γ), C⟨Γ'⟩.
Proof.
intros Γ Γ' A γ.
apply (# (pr1 C) γ A).
Defined.
Definition reindx_structure {CC : precategory}(C : tt_structure CC) :=
∏ (Γ Γ' : CC) (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢rtype A γ⟩.
Definition tt_reindx_struct (CC : precategory) : UU
:=
∑ C : tt_structure CC, reindx_structure C.
Coercion tt_from_tt_reindx CC (C : tt_reindx_struct CC) : tt_structure _ := pr1 C.
Coercion reindx_from_tt_reindx CC (C : tt_reindx_struct CC) : reindx_structure _ := pr2 C.
Notation "A [[ γ ]]" := (rtype A γ) (at level 40).
Definition rterm {CC : precategory}{C : tt_reindx_struct CC}
: ∏ {Γ Γ' : CC} {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩) (γ : Γ' --> Γ), C⟨Γ'⊢ A [[γ]] ⟩
:=
(pr2 C).
Notation "a ⟦ γ ⟧" := (rterm a γ) (at level 40).
Definition reindx_laws_type {CC : precategory}(C : tt_reindx_struct CC) : UU :=
(∏ Γ (A : C⟨Γ⟩), A [[identity Γ]] = A) ×
(∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), A [[γ';;γ]] = A[[γ]][[γ']]).
Definition reindx_laws_type_proof {CC : precategory}(C : tt_reindx_struct CC)
: reindx_laws_type C.
Proof.
split.
- intros. apply (toforallpaths _ _ _ (functor_id (pr1 (pr1 C))_ )).
- intros. apply (toforallpaths _ _ _ (functor_comp (pr1 (pr1 C)) _ _ )).
Defined.
(∏ Γ (A : C⟨Γ⟩), A [[identity Γ]] = A) ×
(∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩), A [[γ';;γ]] = A[[γ]][[γ']]).
Definition reindx_laws_type_proof {CC : precategory}(C : tt_reindx_struct CC)
: reindx_laws_type C.
Proof.
split.
- intros. apply (toforallpaths _ _ _ (functor_id (pr1 (pr1 C))_ )).
- intros. apply (toforallpaths _ _ _ (functor_comp (pr1 (pr1 C)) _ _ )).
Defined.
Reindexing for terms needs transport along reindexing for types
Definition reindx_laws_terms {CC : precategory} (C : tt_reindx_struct CC)
:=
let T:=reindx_laws_type_proof C in
(∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ =
transportf (λ B, C⟨Γ ⊢ B⟩) (!pr1 T _ _) a) ×
(∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩),
a⟦γ';;γ⟧ =
transportf (λ B, C⟨Γ'' ⊢ B⟩) (!pr2 T _ _ _ _ _ _ ) (a⟦γ⟧⟦γ'⟧)).
:=
let T:=reindx_laws_type_proof C in
(∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ =
transportf (λ B, C⟨Γ ⊢ B⟩) (!pr1 T _ _) a) ×
(∏ Γ Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩),
a⟦γ';;γ⟧ =
transportf (λ B, C⟨Γ'' ⊢ B⟩) (!pr2 T _ _ _ _ _ _ ) (a⟦γ⟧⟦γ'⟧)).
Package of reindexing for types and terms
Definition reindx_laws {CC : precategory} (C : tt_reindx_struct CC) : UU :=
reindx_laws_terms C.
Definition reindx_type_id {CC : precategory} {C : tt_reindx_struct CC}
: ∏ Γ (A : C⟨Γ⟩), A [[identity Γ]] = A
:=
(pr1 (reindx_laws_type_proof C)).
Definition reindx_type_comp {CC : precategory} {C : tt_reindx_struct CC}
{Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩)
: A [[γ';;γ]] = A[[γ]][[γ']]
:=
pr2 (reindx_laws_type_proof C) _ _ _ _ _ _ .
Definition reindx_term_id {CC : precategory} {C : tt_reindx_struct CC}
(T : reindx_laws C)
: ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ =
transportf (λ B, C⟨Γ ⊢ B⟩) (! (reindx_type_id _ _ ) ) a
:= pr1 T.
Definition reindx_term_comp {CC : precategory} {C : tt_reindx_struct CC}
(T : reindx_laws C)
: ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩),
a⟦γ';;γ⟧ =
transportf (λ B, C⟨Γ'' ⊢ B⟩) (! (reindx_type_comp _ _ _ ) ) (a⟦γ⟧⟦γ'⟧)
:=
(pr2 T).
reindx_laws_terms C.
Definition reindx_type_id {CC : precategory} {C : tt_reindx_struct CC}
: ∏ Γ (A : C⟨Γ⟩), A [[identity Γ]] = A
:=
(pr1 (reindx_laws_type_proof C)).
Definition reindx_type_comp {CC : precategory} {C : tt_reindx_struct CC}
{Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (A : C⟨Γ⟩)
: A [[γ';;γ]] = A[[γ]][[γ']]
:=
pr2 (reindx_laws_type_proof C) _ _ _ _ _ _ .
Definition reindx_term_id {CC : precategory} {C : tt_reindx_struct CC}
(T : reindx_laws C)
: ∏ Γ (A : C⟨Γ⟩) (a : C⟨Γ⊢A⟩), a⟦identity Γ⟧ =
transportf (λ B, C⟨Γ ⊢ B⟩) (! (reindx_type_id _ _ ) ) a
:= pr1 T.
Definition reindx_term_comp {CC : precategory} {C : tt_reindx_struct CC}
(T : reindx_laws C)
: ∏ {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') {A : C⟨Γ⟩} (a : C⟨Γ⊢A⟩),
a⟦γ';;γ⟧ =
transportf (λ B, C⟨Γ'' ⊢ B⟩) (! (reindx_type_comp _ _ _ ) ) (a⟦γ⟧⟦γ'⟧)
:=
(pr2 T).
Definition comp_1_struct {CC : precategory} (C : tt_reindx_struct CC) : UU
:=
∏ Γ (A : C⟨Γ⟩), ∑ ΓA, ΓA --> Γ.
Definition tt_reindx_comp_1_struct (CC : precategory) : UU
:=
∑ C : tt_reindx_struct CC, comp_1_struct C.
Coercion tt_reindx_from_tt_reindx_comp_1 (CC : precategory) (C : tt_reindx_comp_1_struct CC)
: tt_reindx_struct _ := pr1 C.
Definition comp_obj {CC : precategory} {C : tt_reindx_comp_1_struct CC} (Γ : CC) (A : C⟨Γ⟩)
: CC
:= (pr1 (pr2 C Γ A)).
Notation "Γ ∙ A" := (comp_obj Γ A) (at level 35).
Definition proj_mor {CC : precategory} {C : tt_reindx_comp_1_struct CC}
{Γ : CC} (A : C⟨Γ⟩)
: Γ ∙ A --> Γ
:= (pr2 (pr2 C Γ A)).
Notation "'π' A" := (proj_mor A) (at level 20).
Definition comp_2_struct {CC : precategory} (C : tt_reindx_comp_1_struct CC) : UU
:=
∏ Γ (A : C⟨Γ⟩),
C⟨(Γ∙A) ⊢ (A [[π A]]) ⟩ ×
(∏ Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢A[[γ]]⟩), Γ' --> Γ∙A).
Definition tt_reindx_type_struct (CC : precategory) : UU
:=
∑ C : tt_reindx_comp_1_struct CC, comp_2_struct C.
Coercion tt_reindx_comp_1_from_tt_reindx_comp (CC : precategory) (C : tt_reindx_type_struct CC)
: tt_reindx_comp_1_struct _ := pr1 C.
Definition gen_elem {CC : precategory} {C : tt_reindx_type_struct CC}
{Γ : CC} (A : C⟨Γ⟩)
: C⟨Γ∙A ⊢ A[[π _ ]]⟩
:=
pr1 (pr2 C Γ A).
Notation "'ν' A" := (gen_elem A) (at level 15).
Definition pairing {CC : precategory} {C : tt_reindx_type_struct CC}
{Γ : CC} {A : C⟨Γ⟩} {Γ'} (γ : Γ' --> Γ) (a : C⟨Γ'⊢A[[γ]]⟩)
: Γ' --> Γ∙A
:= pr2 (pr2 C Γ A) Γ' γ a.
Notation "γ ♯ a" := (pairing γ a) (at level 25).
:=
∏ Γ (A : C⟨Γ⟩),
C⟨(Γ∙A) ⊢ (A [[π A]]) ⟩ ×
(∏ Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢A[[γ]]⟩), Γ' --> Γ∙A).
Definition tt_reindx_type_struct (CC : precategory) : UU
:=
∑ C : tt_reindx_comp_1_struct CC, comp_2_struct C.
Coercion tt_reindx_comp_1_from_tt_reindx_comp (CC : precategory) (C : tt_reindx_type_struct CC)
: tt_reindx_comp_1_struct _ := pr1 C.
Definition gen_elem {CC : precategory} {C : tt_reindx_type_struct CC}
{Γ : CC} (A : C⟨Γ⟩)
: C⟨Γ∙A ⊢ A[[π _ ]]⟩
:=
pr1 (pr2 C Γ A).
Notation "'ν' A" := (gen_elem A) (at level 15).
Definition pairing {CC : precategory} {C : tt_reindx_type_struct CC}
{Γ : CC} {A : C⟨Γ⟩} {Γ'} (γ : Γ' --> Γ) (a : C⟨Γ'⊢A[[γ]]⟩)
: Γ' --> Γ∙A
:= pr2 (pr2 C Γ A) Γ' γ a.
Notation "γ ♯ a" := (pairing γ a) (at level 25).
Definition comp_laws_1_2 {CC : precategory} {C : tt_reindx_type_struct CC}
(L : reindx_laws C) : UU :=
∏ Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩),
∑ h : (γ ♯ a) ;; (π _ ) = γ,
transportf (λ ι, C⟨Γ'⊢ A [[ι]]⟩) h
(transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp (π _ )(γ ♯ a) _ )
((ν _ ) ⟦γ ♯ a⟧)) = a.
Definition comp_law_3 {CC : precategory} {C : tt_reindx_type_struct CC}
(L : reindx_laws C) : UU
:=
∏ Γ (A : C ⟨Γ⟩) Γ' Γ'' (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') (a : C⟨Γ'⊢ A[[γ]]⟩),
γ' ;; (γ ♯ a)
=
(γ' ;; γ) ♯ (transportf (λ B, C⟨Γ''⊢ B⟩) (!reindx_type_comp γ γ' _ ) (a⟦γ'⟧)).
Definition comp_law_4 {CC : precategory} {C : tt_reindx_type_struct CC}
(L : reindx_laws C) : UU
:=
∏ Γ (A : C⟨Γ⟩), π A ♯ ν A = identity _ .
Definition cwf_laws {CC : precategory}(C : tt_reindx_type_struct CC)
:=
(∑ T : reindx_laws C,
(comp_laws_1_2 T × comp_law_3 T × comp_law_4 T)) ×
(has_homsets CC × ∏ Γ (A : C⟨Γ⟩), isaset (C⟨Γ⊢ A⟩)).
Definition of precategory with families
A precategory with families pre_cwf is- a precategory
- with type-and-term structure
- with reindexing
- with comprehension structure
- satisfying the comprehension laws
- where types and terms are hsets
Various access functions to the components
Also a few generalizations are proved, providing variants with generalized proofs of identity of types, terms (which form hsets)Coercion cwf_data_from_cwf_struct (CC : precategory) (C : cwf_struct CC) : _ CC := pr1 C.
Coercion cwf_laws_from_cwf_struct (CC : precategory) (C : cwf_struct CC) : cwf_laws C := pr2 C.
Coercion reindx_laws_from_cwf_struct (CC : precategory) (C : cwf_struct CC)
: reindx_laws C
:= pr1 (pr1 (pr2 C)).
Definition cwf_comp_laws {CC : precategory} (C : cwf_struct CC)
: (comp_laws_1_2 C × comp_law_3 C × comp_law_4 C)
:= pr2 (pr1 (pr2 C)).
Definition has_homsets_cwf {CC : precategory} (C : cwf_struct CC) : has_homsets CC
:= pr1 (pr2 (pr2 C)).
Definition cwf_types_isaset {CC : precategory} (C : cwf_struct CC) Γ : isaset (C⟨Γ⟩)
:= setproperty (C⟨Γ⟩).
Definition cwf_terms_isaset {CC : precategory} (C : cwf_struct CC) : ∏ Γ A, isaset (C⟨Γ ⊢ A⟩)
:= (pr2 (pr2 (pr2 C))).
Definition cwf_law_1 {CC : precategory} (C : cwf_struct CC)
Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩)
: (γ ♯ a) ;; (π _) = γ
:= pr1 (pr1 (cwf_comp_laws C) Γ A Γ' γ a).
Definition cwf_law_2 {CC : precategory} (C : cwf_struct CC)
Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩)
: transportf (λ ι, C⟨Γ'⊢ A [[ι]]⟩) (cwf_law_1 C Γ A Γ' γ a)
(transportf (λ B, C⟨Γ'⊢ B⟩) (!reindx_type_comp (π _)(γ ♯ a) _ )
((ν A) ⟦γ ♯ a⟧))
= a
:= pr2 ((pr1 (cwf_comp_laws C)) Γ A Γ' γ a).
Definition cwf_law_2_gen {CC : precategory} (C : cwf_struct CC)
Γ (A : C ⟨Γ⟩) Γ' (γ : Γ' --> Γ) (a : C⟨Γ'⊢ A[[γ]]⟩)
: ∏ (p : (A [[π A]]) [[γ ♯ a]] = A [[γ ♯ a;; π A]]) (p0 : γ ♯ a;; π A = γ),
transportf (λ ι : Γ' --> Γ, C ⟨ Γ' ⊢ A [[ι]] ⟩) p0
(transportf (λ B : C ⟨ Γ' ⟩, C ⟨ Γ' ⊢ B ⟩) p (ν A ⟦ γ ♯ a ⟧)) = a.
Proof.
intros p p'.
etrans; [ | apply cwf_law_2].
match goal with | [ |- _ = transportf _ ?p1 _ ] => assert (T : p' = p1) end.
{ apply (has_homsets_cwf C). }
rewrite T; clear T. apply maponpaths.
match goal with | [ |- _ = transportf _ ?p1 _ ] => assert (T : p = p1) end.
{ apply (cwf_types_isaset C). }
rewrite T; apply idpath.
Qed.
Definition cwf_law_3 {CC : precategory} (C : cwf_struct CC) : comp_law_3 C
:= pr1 (pr2 (cwf_comp_laws C)).
Definition cwf_law_3_gen {CC : precategory} (C : cwf_struct CC)
(Γ : CC) (A : C ⟨ Γ ⟩) (Γ' Γ'' : CC) (γ : Γ' --> Γ) (γ' : Γ'' --> Γ')
(a : C ⟨ Γ' ⊢ A [[γ]] ⟩) (p : (A [[γ]]) [[γ']] = A [[γ';; γ]]):
γ';; γ ♯ a =
(γ';; γ) ♯ transportf (λ B : C ⟨ Γ'' ⟩, C ⟨ Γ'' ⊢ B ⟩) p (a ⟦ γ' ⟧).
Proof.
etrans. apply cwf_law_3.
apply maponpaths.
match goal with |[|- transportf _ ?e _ = _ ] => assert (T : e = p) end.
{ apply (cwf_types_isaset C). }
rewrite T; apply idpath.
Qed.
Definition cwf_law_4 {CC : precategory} (C : cwf_struct CC) : comp_law_4 C
:= pr2 (pr2 (cwf_comp_laws C)).
Ltac imp := apply impred; intro.
Lemma isPredicate_cwf_laws (CC : precategory)
: isPredicate (@cwf_laws CC).
Proof.
intros T.
apply isofhlevelsn.
intro H.
set (X:= tpair _ T H : cwf_struct CC).
apply (isofhleveltotal2).
- apply isofhleveltotal2.
+ apply isofhleveltotal2.
* intros.
do 3 imp. apply (cwf_terms_isaset X).
* intros.
do 7 imp. apply (cwf_terms_isaset X).
+ intros.
repeat (apply isofhleveldirprod).
*
{
do 5 imp.
apply (isofhleveltotal2 1).
- apply (has_homsets_cwf X).
- intros. apply (cwf_terms_isaset X).
}
* do 7 imp. apply (has_homsets_cwf X).
* do 2 imp. apply (has_homsets_cwf X).
- intros.
repeat (apply isofhleveldirprod).
+ apply isaprop_has_homsets.
+ do 2 imp. apply isapropisaset.
Qed.
Section CwF_lemmas.
Generalizable Variable CC.
Context `{C : cwf_struct CC}.
Lemma map_to_comp_as_pair_precwf {Γ} {A : C⟨Γ⟩} {Γ'} (f : Γ' --> Γ∙A)
: (f ;; π A) ♯ (transportb _ (reindx_type_comp _ _ _) ((gen_elem A)⟦f⟧))
=
f.
Proof.
sym.
etrans.
apply (!id_right _ ).
etrans.
refine (maponpaths (fun g => f ;; g) (!cwf_law_4 _ _ _)).
apply cwf_law_3.
Qed.
Lemma retype_term_pi {Γ} {A A' : C ⟨ Γ ⟩ } (p : A = A') (t : C ⟨ Γ ∙ A ⊢ A [[π A]]⟩ ) :
transportf (λ B : C ⟨Γ⟩, C ⟨ Γ ∙ A ⊢ B [[π A]]⟩) p t
=
transportf (term C (Γ ∙ A)) (maponpaths (λ x : C⟨Γ⟩, x [[π A]]) p) t.
Proof.
destruct p.
apply idpath.
Defined.
Lemma pairing_mapeq {Γ} {A : C⟨Γ⟩} {Γ'} (f f' : Γ' --> Γ) (e : f = f')
(a : C ⟨ Γ' ⊢ A [[f]] ⟩)
: f ♯ a
=
f' ♯ (transportf (fun B => C⟨Γ' ⊢ B⟩ ) (maponpaths _ e) a).
Proof.
destruct e. apply idpath.
Qed.
Lemma pairing_mapeq_gen {Γ} {Γ'} (f f' : Γ' --> Γ) {A : C⟨Γ⟩} (a : C ⟨ Γ' ⊢ A [[f]] ⟩)
(e : f = f') (p : A [[f]] = A [[f']])
: f ♯ a
=
f' ♯ (transportf (fun B => C⟨Γ' ⊢ B⟩ ) p a).
Proof.
assert (T : p = (maponpaths _ e)).
{ apply (cwf_types_isaset C). }
rewrite T.
apply pairing_mapeq.
Qed.
Lemma rterm_typeeq {Γ} {A A': C⟨Γ⟩} (e : A = A') {Γ'} (f : Γ' --> Γ) (x : C ⟨ Γ ⊢ A ⟩)
: transportf _ (maponpaths (fun b => b[[f]]) e) (x⟦f⟧)
= (transportf _ e x) ⟦f⟧.
Proof.
destruct e. apply idpath.
Qed.
Lemma transportf_rtype_mapeq {Γ} {A : C⟨Γ⟩} {Γ'} (f f' : Γ' --> Γ) (e : f = f')
(t : C ⟨ Γ' ⊢ A[[f]] ⟩)
: transportf (fun g => C ⟨ Γ' ⊢ A[[g]] ⟩) e t
= transportf _ (maponpaths (fun g => A[[g]]) e) t.
Proof.
apply functtransportf.
Qed.
Lemma rterm_mapeq {Γ} {A : C⟨Γ⟩} {Γ'} {f f' : Γ' --> Γ} (e : f = f') (t : C ⟨ Γ ⊢ A ⟩)
: t ⟦ f ⟧
= transportb _ (maponpaths (fun g => A[[g]]) e) (t ⟦ f'⟧ ).
Proof.
destruct e. apply idpath.
Qed.
Lemma term_typeeq_transport_lemma {Γ} {A A' A'': C ⟨ Γ ⟩} (e : A = A'') (e' : A' = A'')
(x : C ⟨ Γ ⊢ A ⟩) (x' : C ⟨ Γ ⊢ A' ⟩)
: transportf _ (e @ !e') x = x'
-> transportf _ e x = transportf _ e' x'.
Proof.
apply transportf_comp_lemma.
Qed.
Lemma term_typeeq_transport_lemma_2 {Γ} {A : C ⟨ Γ ⟩} (e : A = A)
{x x' : C ⟨ Γ ⊢ A ⟩}
: x = x'
-> transportf _ e x = x'.
Proof.
apply transportf_comp_lemma_hset.
apply cwf_types_isaset.
Qed.
Lemma reindx_term_comp' {Γ Γ' Γ''} (γ : Γ' --> Γ) (γ' : Γ'' --> Γ') {A} (a : C ⟨ Γ ⊢ A ⟩)
: transportf _ (reindx_type_comp _ _ _) (a ⟦ γ' ;; γ ⟧)
= ((a ⟦ γ ⟧) ⟦ γ' ⟧).
Proof.
eapply pathscomp0.
apply maponpaths, (reindx_term_comp C).
rew_trans_@.
apply term_typeeq_transport_lemma_2.
apply idpath.
Qed.
Definition pre_cwf_law_2' Γ (A : C ⟨ Γ ⟩) Γ' (γ : Γ' --> Γ) (a : C ⟨ Γ' ⊢ A[[γ]] ⟩)
: (ν A) ⟦γ ♯ a⟧
= transportf _ (reindx_type_comp _ _ _)
(transportb _ (maponpaths (fun g => A[[g]]) (cwf_law_1 _ _ _ _ _ _))
a).
Proof.
eapply pathscomp0. Focus 2.
apply maponpaths, maponpaths. exact (cwf_law_2 _ _ _ _ γ a).
apply pathsinv0.
rew_trans_@.
etrans. apply maponpaths, transportf_rtype_mapeq.
rew_trans_@.
refine (@maponpaths _ _ (fun e => transportf _ e _) _ (idpath _) _).
apply cwf_types_isaset.
Qed.
Definition pairing_transport {Γ} {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.
Definition q_precwf {Γ} (A : C ⟨ Γ ⟩ ) {Γ'} (f : Γ' --> Γ)
: (comp_obj Γ' (A[[f]])) --> (Γ ∙ A).
Proof.
set (T:= @pairing _ C).
apply T with (γ := π _ ;; f).
refine (transportb (term C (Γ' ∙ (A [[f]])) ) (reindx_type_comp _ _ A) _).
apply gen_elem.
Defined.
Definition dpr_q_precwf
{Γ} (A : C ⟨ Γ ⟩)
{Γ'} (f : Γ' --> Γ)
: (q_precwf A f) ;; (π A) = (π (A[[f]])) ;; f.
Proof.
unfold q_precwf.
apply cwf_law_1.
Qed.
Lemma rterm_univ {Γ} {A : C ⟨ Γ ⟩} {Γ'} (f : Γ' --> Γ)
: ν (A[[f]])
= transportf _ (reindx_type_comp _ _ _)
(transportf _ (maponpaths (fun g => A[[g]]) (dpr_q_precwf A f))
(transportb _ (reindx_type_comp _ _ _)
((ν A)⟦q_precwf A f⟧))).
Proof.
sym.
rew_trans_@.
etrans.
- apply maponpaths.
apply pre_cwf_law_2'.
- rew_trans_@.
apply term_typeeq_transport_lemma_2.
apply idpath.
Qed.
The biggest work is in showing that the square of dependent projections/reindexings is a pullback.
We split this up into several lemmas:
- construction of the pullback pairing function;
- proof that projections applied to the pairing recover the original maps;
- and proof that the pairing map is the unique such map.
Definition dpr_q_pbpairing_precwf_aux
{Γ} (A : C ⟨ Γ ⟩)
{Γ'} (f : Γ' --> Γ)
{X} (h : X --> Γ ∙ A) (k : X --> Γ') (H : h ;; π A = k ;; f)
: C ⟨ X ⊢ (A [[f]]) [[k]] ⟩
:= (transportf _ (reindx_type_comp _ _ _)
(transportf (fun g => C ⟨ X ⊢ A[[g]] ⟩) H
(transportf _ (!reindx_type_comp _ _ _)
((ν A)⟦h⟧)))).
Definition dpr_q_pbpairing_commutes
{Γ} (A : C ⟨ Γ ⟩)
{Γ'} (f : Γ' --> Γ)
{X} (h : X --> Γ ∙ A) (k : X --> Γ') (H : h ;; π A = k ;; f)
(hk := @pairing _ C Γ' (A[[f]]) X k (dpr_q_pbpairing_precwf_aux A f h k H))
: (hk ;; q_precwf A f = h) × (hk ;; π (A[[f]]) = k).
Proof.
split. Focus 2. apply cwf_law_1.
unfold q_precwf.
etrans. Focus 2.
apply map_to_comp_as_pair_precwf.
etrans.
apply cwf_law_3.
assert ((k ♯ (dpr_q_pbpairing_precwf_aux A f h k H)) ;; (π (A [[f]]) ;; f)
= h ;; π A) as e1.
eapply pathscomp0. apply assoc.
refine (_ @ !H).
apply (maponpaths (fun g => g ;; f)).
apply cwf_law_1.
eapply pathscomp0. apply (pairing_mapeq _ _ e1).
apply maponpaths.
eapply pathscomp0. apply transport_f_f.
eapply pathscomp0. apply maponpaths. refine (! rterm_typeeq _ _ _).
eapply pathscomp0. apply transport_f_f.
eapply pathscomp0. apply maponpaths, pre_cwf_law_2'.
rew_trans_@.
eapply pathscomp0. apply maponpaths, transportf_rtype_mapeq.
repeat (eapply pathscomp0; [ apply transport_f_f | ]).
refine (maponpaths (fun e => transportf _ e _) _).
apply cwf_types_isaset.
Qed.
Definition dpr_q_pbpairing_precwf
{Γ} (A : C ⟨ Γ ⟩)
{Γ'} (f : Γ' --> Γ)
{X} (h : X --> Γ ∙ A) (k : X --> Γ') (H : h ;; π A = k ;; f)
: ∑ (hk : X --> Γ' ∙ (A[[f]])),
( hk ;; q_precwf A f = h
× hk ;; π (A[[f]]) = k).
Proof.
exists (@pairing _ C Γ' (A[[f]]) X k (dpr_q_pbpairing_precwf_aux A f h k H)).
apply dpr_q_pbpairing_commutes.
Defined.
Definition dpr_q_pbpairing_precwf_mapunique
{Γ} (A : C⟨Γ⟩)
{Γ'} (f : Γ' --> Γ)
{X} {h : X --> Γ ∙ A} {k : X --> Γ'} (H : h ;; π A = k ;; f)
(hk : X --> Γ' ∙ (A [[f]]))
(e2 : hk ;; q_precwf A f = h)
(e1 : hk ;; π (A[[f]]) = k)
: hk = pr1 (dpr_q_pbpairing_precwf A f h k H).
Proof.
eapply pathscomp0.
eapply pathsinv0. apply map_to_comp_as_pair_precwf.
eapply pathscomp0.
apply (pairing_mapeq _ _ e1 _).
simpl. apply maponpaths.
eapply pathscomp0.
apply maponpaths, maponpaths.
apply (@maponpaths (C ⟨ Γ' ∙ (A[[f]]) ⊢ A[[f]][[π (A[[f]])]] ⟩) _ (fun t => t ⟦hk⟧)).
apply rterm_univ.
eapply pathscomp0.
apply maponpaths, maponpaths.
eapply pathscomp0.
symmetry. apply rterm_typeeq.
apply maponpaths.
eapply pathscomp0.
symmetry. apply rterm_typeeq.
apply maponpaths.
eapply pathscomp0.
symmetry. apply rterm_typeeq.
apply maponpaths.
symmetry. apply reindx_term_comp'.
apply term_typeeq_transport_lemma.
repeat (eapply pathscomp0; [ apply transport_f_f |]).
eapply pathscomp0.
apply maponpaths, (rterm_mapeq e2).
eapply pathscomp0. apply transport_f_f.
eapply pathscomp0.
Focus 2. symmetry. apply transportf_rtype_mapeq.
repeat apply term_typeeq_transport_lemma.
apply term_typeeq_transport_lemma_2.
apply idpath.
Qed.
Definition dpr_q_pbpairing_precwf_unique (hs : has_homsets CC)
{Γ} (A : C⟨Γ⟩)
{Γ'} (f : Γ' --> Γ)
{X} (h : X --> Γ ∙ A) (k : X --> Γ') (H : h ;; π A = k ;; f)
(t : ∑ hk : X --> Γ' ∙ (A [[f]]),
(hk ;; q_precwf A f = h) × (hk ;; π (A[[f]]) = k))
: t = dpr_q_pbpairing_precwf A f h k H.
Proof.
destruct t as [hk [e2 e1] ].
unshelve refine (@total2_paths_f _ _ (tpair _ hk (tpair _ e2 e1)) _
(dpr_q_pbpairing_precwf_mapunique A f H hk e2 e1) _).
unshelve refine (total2_paths_f _ _); apply hs.
Qed.
Lemma is_pullback_reindx_cwf (hs : has_homsets CC) : ∏ (Γ : CC) (A : C⟨Γ⟩) (Γ' : CC)
(f : Γ' --> Γ),
isPullback (π A) f (q_precwf A f) (π (A [[f]])) (dpr_q_precwf A f).
Proof.
intros.
apply mk_isPullback; try assumption.
intros e h k H.
exists (dpr_q_pbpairing_precwf _ _ h k H).
apply dpr_q_pbpairing_precwf_unique.
assumption.
Defined.
End CwF_lemmas.