Skip to content

Commit 490c7d4

Browse files
VojtechStepVojtechStep
committed
Progress
1 parent c2d1801 commit 490c7d4

File tree

2 files changed

+239
-40
lines changed

2 files changed

+239
-40
lines changed

‎src/synthetic-homotopy-theory/functoriality-stuff.lagda.md

Lines changed: 238 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -869,50 +869,95 @@ module _
869869

870870
```agda
871871
module _
872-
{l1 l2 l3 l4 l5 l6 l7 : Level}
873-
{A : UU l1} {B : UU l2} {C : UU l3} {D : UU l7}
874-
{P : A → UU l4} {P' : B → UU l5} {Q' : C → UU l6}
875-
{h : A → B} (h' : (a : A) → P a → P' (h a))
876-
{l : A → D} (j : D → C) (l' : (a : A) → P a → Q' (j (l a)))
877-
(s : (a : A) → P' (h a) → Q' (j (l a)))
878-
{k : D → B} (t : (a : A) → Q' (j (l a)) → P' (k (l a)))
879-
(U : h ~ k ∘ l)
880-
(H : (a : A) (p : P a) → l' a p ＝ s a (h' a p))
881-
(K : (a : A) (p : P' (h a)) → t a (s a p) ＝ tr P' (U a) p)
872+
{l1 l2 : Level}
873+
{A : UU l1}
874+
{P : A → UU l2}
882875
where
883876
open import foundation.dependent-identifications
884877
885-
compute-lemma :
886-
(a : A) (p : P a) →
887-
inv-dependent-identification P' (U a)
888-
( inv
889-
( ap (t a) (H a p) ∙
890-
K a (h' a p))) ＝
891-
ap
892-
( tr P' (inv (U a)) ∘ t a)
893-
( H a p) ∙
894-
inv-dependent-identification P' (U a)
895-
( inv (K a (h' a p)))
896-
compute-lemma a p =
897-
compute-inv-dependent-identification (U a) _ ∙
878+
compute-lemma'' :
879+
{x y : A} (p : x ＝ y) →
880+
{x' : P x} {y' z' : P y}
881+
(K : dependent-identification P p x' y')
882+
(H : y' ＝ z') →
883+
inv-dependent-identification P p (K ∙ H) ＝
898884
ap
899-
( map-eq-transpose-equiv-inv' (equiv-tr P' (U a)))
900-
( inv-inv _) ∙
885+
( tr P (inv p))
886+
( inv H) ∙
887+
inv-dependent-identification P p K
888+
compute-lemma'' refl K refl = ap inv right-unit
889+
890+
module _
891+
{l1 l2 l5 l6 : Level}
892+
{A : UU l1} {B : UU l2}
893+
{P : A → UU l5} {Q : UU l6} -- {Q : B → UU l6}
894+
where
895+
open import foundation.dependent-identifications
896+
897+
compute-lemma :
898+
{x y : A} (p : x ＝ y) →
899+
{u v : Q} (H : u ＝ v) →
900+
(f : Q → P y)
901+
{x' : P x} (K : dependent-identification P p x' (f u)) →
902+
inv-dependent-identification P p (K ∙ ap f H) ＝
901903
ap
902-
( _∙ is-retraction-map-inv-equiv (equiv-tr P' (U a)) _)
903-
( ap-concat (tr P' (inv (U a))) _ _) ∙
904-
assoc _ _ _ ∙
904+
( tr P (inv p) ∘ f)
905+
( inv H) ∙
906+
inv-dependent-identification P p K
907+
compute-lemma p H f K =
908+
compute-lemma'' p K (ap f H) ∙
905909
ap
906-
(_∙ map-eq-transpose-equiv-inv' (equiv-tr P' (U a)) (K a (h' a p)))
907-
( inv (ap-comp (tr P' (inv (U a))) (t a) (H a p))) ∙
910+
( _∙ inv-dependent-identification P p K)
911+
( ap
912+
( ap (tr P (inv p)))
913+
( inv (ap-inv f H)) ∙
914+
inv (ap-comp (tr P (inv p)) f (inv H)))
915+
916+
compute-lemma' :
917+
{x y : A} (p : x ＝ y) →
918+
{u v : Q} (H : u ＝ v) →
919+
(f : Q → P y) →
920+
{x' : P x} (K : f v ＝ tr P p x') →
921+
inv-dependent-identification P p (inv (ap f H ∙ K)) ＝
908922
ap
909-
( ap (tr P' (inv (U a)) ∘ t a) (H a p) ∙_)
910-
( inv
911-
( compute-inv-dependent-identification (U a) _ ∙
912-
ap (map-eq-transpose-equiv-inv' (equiv-tr P' (U a))) (inv-inv _)))
923+
( tr P (inv p) ∘ f)
924+
( H) ∙
925+
inv-dependent-identification P p (inv K)
926+
compute-lemma' refl refl f K = refl
927+
-- ap
928+
-- ( inv-dependent-identification P p)
929+
-- ( distributive-inv-concat (ap f H) K ∙ ap (inv K ∙_) (inv (ap-inv f H))) ∙
930+
-- compute-lemma p (inv H) f (inv K) ∙
931+
-- ap
932+
-- ( λ r → ap (tr P (inv p) ∘ f) r ∙ inv-dependent-identification P p (inv K))
933+
-- ( inv-inv H)
913934
```
914935

915936
```agda
937+
938+
module _
939+
{l1 l2 l3 l4 : Level}
940+
{A : UU l1} {B : A → UU l2}
941+
{X : UU l3} {Y : X → UU l4}
942+
where
943+
944+
compute-left-whisker-transpose :
945+
{s : A → X} (s' : {a : A} → B a → Y (s a))
946+
{x y : A} (p : y ＝ x)
947+
{x' : B x} {y' : B y} (p' : x' ＝ tr B p y') →
948+
left-whisk-dependent-identification {B' = Y} s' (inv p)
949+
( map-eq-transpose-equiv-inv' (equiv-tr B p) p') ＝
950+
ap
951+
( λ r → tr Y r (s' x'))
952+
( ap-inv s p) ∙
953+
inv
954+
( map-eq-transpose-equiv
955+
( equiv-tr Y (ap s p))
956+
( left-whisk-dependent-identification {B' = Y} s' p
957+
( inv p')))
958+
compute-left-whisker-transpose s' refl refl =
959+
inv (ap inv (compute-refl-eq-transpose-equiv id-equiv))
960+
916961
open import synthetic-homotopy-theory.zigzags-sequential-diagrams
917962
module _
918963
{l1 l2 l3 l4 l5 : Level}
@@ -972,8 +1017,53 @@ module _
9721017
tr
9731018
( family-descent-data-sequential-colimit P' (succ-ℕ n))
9741019
( upper-triangle-zigzag-sequential-diagram z n a)
975-
inv-upper-triangle-over' n a =
976-
{!!}
1020+
inv-upper-triangle-over' n a p =
1021+
inv
1022+
( ( preserves-tr
1023+
( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n))
1024+
( upper-triangle-zigzag-sequential-diagram z n a)
1025+
( p)) ∙
1026+
( inv
1027+
( substitution-law-tr
1028+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1029+
( map-zigzag-sequential-diagram z (succ-ℕ n))
1030+
( upper-triangle-zigzag-sequential-diagram z n a))) ∙
1031+
( ap
1032+
( λ r →
1033+
tr
1034+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1035+
( r)
1036+
( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n)
1037+
( map-sequential-diagram A n a)
1038+
( p)))
1039+
( inv
1040+
( ap
1041+
( _∙ lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))
1042+
( distributive-inv-concat
1043+
( lower-triangle-zigzag-sequential-diagram z n
1044+
( map-zigzag-sequential-diagram z n a))
1045+
( ap
1046+
( map-zigzag-sequential-diagram z (succ-ℕ n))
1047+
( inv (upper-triangle-zigzag-sequential-diagram z n a)))) ∙
1048+
assoc _ _ _ ∙
1049+
ap
1050+
( inv (ap (map-zigzag-sequential-diagram z (succ-ℕ n)) (inv (upper-triangle-zigzag-sequential-diagram z n a))) ∙_)
1051+
( left-inv (lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))) ∙
1052+
right-unit ∙
1053+
ap inv (ap-inv _ _) ∙
1054+
inv-inv _))) ∙
1055+
( tr-concat
1056+
( inv (naturality-map-hom-diagram-zigzag-sequential-diagram z n a))
1057+
( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))
1058+
( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) (map-sequential-diagram A n a) p)))
1059+
-- inv
1060+
-- ( tr-concat
1061+
-- ( inv (naturality-map-hom-diagram-zigzag-sequential-diagram z n a))
1062+
-- ( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))
1063+
-- ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) (map-sequential-diagram A n a) p)) ∙
1064+
-- {!preserves-tr
1065+
-- ( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n))
1066+
-- ( )!}
9771067
9781068
opaque
9791069
upper-triangle-over' :
@@ -1008,8 +1098,7 @@ module _
10081098
( inv-map-over-diagram-equiv-zigzag n (map-zigzag-sequential-diagram z n a))
10091099
inv-upper-triangle-over n a p =
10101100
ap
1011-
( map-inv-fam-equiv e _ ∘
1012-
tr Q (inv (C (succ-ℕ n) _)) ∘
1101+
( inv-map-over-diagram-equiv-zigzag' (succ-ℕ n) _ ∘
10131102
tr
10141103
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
10151104
( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a)))
@@ -1077,6 +1166,65 @@ module _
10771166
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
10781167
( lower-triangle-zigzag-sequential-diagram z n b)
10791168
( map-family-descent-data-sequential-colimit Q' n b q))
1169+
1170+
trivial-pasting :
1171+
(n : ℕ) →
1172+
htpy-over
1173+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1174+
( naturality-map-hom-diagram-zigzag-sequential-diagram z n)
1175+
( tr
1176+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1177+
( inv (naturality-map-hom-diagram-zigzag-sequential-diagram z n _)) ∘
1178+
map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) _)
1179+
( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) _)
1180+
trivial-pasting n =
1181+
concat-htpy-over
1182+
( lower-triangle-zigzag-sequential-diagram z n ·r
1183+
( map-zigzag-sequential-diagram z n))
1184+
( ( map-zigzag-sequential-diagram z (succ-ℕ n)) ·l
1185+
( inv-htpy (upper-triangle-zigzag-sequential-diagram z n)))
1186+
( λ p →
1187+
lower-triangle-over' (succ-ℕ n) _
1188+
( tr
1189+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1190+
( lower-triangle-zigzag-sequential-diagram z n _)
1191+
( tr
1192+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1193+
( inv (naturality-map-hom-diagram-zigzag-sequential-diagram z n _))
1194+
( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n)
1195+
( map-sequential-diagram A n _)
1196+
( p)))))
1197+
( left-whisk-htpy-over
1198+
( inv-htpy (upper-triangle-zigzag-sequential-diagram z n))
1199+
( λ p →
1200+
map-eq-transpose-equiv-inv'
1201+
( equiv-tr
1202+
( family-descent-data-sequential-colimit P' (succ-ℕ n))
1203+
( upper-triangle-zigzag-sequential-diagram z n _))
1204+
( upper-triangle-over' n _ p))
1205+
( map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) _))
1206+
1207+
abstract
1208+
open import foundation.dependent-identifications
1209+
is-trivial-trivial-pasting :
1210+
(n : ℕ) (a : family-sequential-diagram A n) →
1211+
trivial-pasting n {a} ~
1212+
is-section-map-inv-equiv
1213+
( equiv-tr
1214+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1215+
( naturality-map-hom-diagram-zigzag-sequential-diagram z n a)) ·r
1216+
map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) (map-sequential-diagram A n a)
1217+
is-trivial-trivial-pasting n a p =
1218+
ap
1219+
( λ K' →
1220+
concat-dependent-identification _ _ _
1221+
( lower-triangle-over' (succ-ℕ n) _ _)
1222+
( K'))
1223+
( compute-left-whisker-transpose
1224+
( λ {a} → map-over-diagram-equiv-over-colimit up-c c' f P Q e (succ-ℕ n) a)
1225+
( upper-triangle-zigzag-sequential-diagram z n a)
1226+
( upper-triangle-over' n a p)) ∙
1227+
{!!}
10801228
```
10811229

10821230
```agda
@@ -1138,7 +1286,7 @@ module _
11381286
11391287
opaque
11401288
-- TODO: Maybe this goes through for general equivalences immediately?
1141-
-- I haven't tried
1289+
-- I haven't tried yet
11421290
compute-square-over-zigzag-square-over-colimit-id :
11431291
(n : ℕ) (a : family-sequential-diagram A n) →
11441292
pasting-triangles-over
@@ -1326,7 +1474,57 @@ module _
13261474
assoc _ _ _ ∙
13271475
ap
13281476
( square-over-diagram-square-over-colimit up-c c' f P Q id-fam-equiv n a p ∙_)
1329-
( {!!}) ∙
1477+
( ap
1478+
( inv
1479+
( is-section-map-inv-equiv
1480+
( equiv-tr
1481+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1482+
( naturality-map-hom-diagram-zigzag-sequential-diagram z n a))
1483+
( map-over-diagram-equiv-over-colimit up-c c' f P Q id-fam-equiv (succ-ℕ n)
1484+
( map-sequential-diagram A n a)
1485+
( map-family-descent-data-sequential-colimit P' n a p))) ∙_)
1486+
( assoc _ _ _ ∙
1487+
inv
1488+
( compute-concat-dependent-identification
1489+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1490+
( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))
1491+
( ap (map-zigzag-sequential-diagram z (succ-ℕ n)) (inv (upper-triangle-zigzag-sequential-diagram z n a)))
1492+
( lower-triangle-over' up-c c' z P Q id-fam-equiv (succ-ℕ n)
1493+
( inv-map-zigzag-sequential-diagram z n
1494+
( map-zigzag-sequential-diagram z n a))
1495+
( tr
1496+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1497+
( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))
1498+
( tr
1499+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1500+
( inv (naturality-map-hom-diagram-zigzag-sequential-diagram z n a))
1501+
( map-over-diagram-equiv-over-colimit up-c c' f P Q id-fam-equiv (succ-ℕ n)
1502+
( map-sequential-diagram A n a)
1503+
( map-family-descent-data-sequential-colimit P' n a p)))))
1504+
( _)) ∙
1505+
ap
1506+
( concat-dependent-identification
1507+
( family-descent-data-sequential-colimit Q' (succ-ℕ n))
1508+
( lower-triangle-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))
1509+
( ap
1510+
( map-zigzag-sequential-diagram z (succ-ℕ n))
1511+
( inv (upper-triangle-zigzag-sequential-diagram z n a)))
1512+
( lower-triangle-over' up-c c' z P Q id-fam-equiv (succ-ℕ n)
1513+
( inv-map-zigzag-sequential-diagram z n (map-zigzag-sequential-diagram z n a))
1514+
( _)))
1515+
( inv
1516+
( compute-left-whisk-dependent-identification
1517+
( map-over-diagram-equiv-over-colimit up-c c' f P Q id-fam-equiv (succ-ℕ n) _)
1518+
( inv (upper-triangle-zigzag-sequential-diagram z n a))
1519+
( map-eq-transpose-equiv-inv'
1520+
( equiv-tr
1521+
( family-descent-data-sequential-colimit P' (succ-ℕ n))
1522+
( upper-triangle-zigzag-sequential-diagram z n a))
1523+
( upper-triangle-over' up-c c' z P Q id-fam-equiv n a
1524+
( map-family-descent-data-sequential-colimit P' n _ p))))) ∙
1525+
is-trivial-trivial-pasting up-c c' z P Q id-fam-equiv n a
1526+
( map-family-descent-data-sequential-colimit P' n _ p)) ∙
1527+
( left-inv _)) ∙
13301528
right-unit
13311529
```
13321530

‎src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ open import foundation.structure-identity-principle
2424
open import foundation.torsorial-type-families
2525
open import foundation.universe-levels
2626
open import foundation.whiskering-homotopies-composition
27+
open import foundation.whiskering-homotopies-concatenation
2728
2829
open import synthetic-homotopy-theory.dependent-sequential-diagrams
2930
open import synthetic-homotopy-theory.sequential-diagrams

0 commit comments

Comments
 (0)