Add equifibered dependent span diagrams and improve universe polymorphism for descent data of pushouts

codespell-dictionary.txt

@@ -4,39 +4,55 @@ Kuratowsky->Kuratowski
 Lavwere->Lawvere
 anamorhpism->anamorphism
 anamorhpisms->anamorphisms
+anamorhpsim->anamorphism
+anamorhpsims->anamorphisms
 anamorphsim->anamorphism
 anamorphsim->anamorphism
 anamorphsims->anamorphisms
 automorhpism->automorphism
 automorhpisms->automorphisms
+automorhpsim->automorphism
+automorhpsims->automorphisms
 automorphsim->automorphism
 automorphsims->automorphisms
 cagegory->category
 consistsing->consisting
 eacy->each,easy
 endomorhpism->endomorphism
 endomorhpisms->endomorphisms
+endomorhpsim->endomorphism
+endomorhpsims->endomorphisms
 endomorphsim->endomorphism
 endomorphsims->endomorphisms
 epimorhpism->epimorphism
 epimorhpisms->epimorphisms
+epimorhpsim->epimorphism
+epimorhpsims->epimorphisms
 epimorphsim->epimorphism
 epimorphsims->epimorphisms
 foundaiton->foundation
 homomorhpism->homomorphism
 homomorhpisms->homomorphisms
+homomorhpsim->homomorphism
+homomorhpsims->homomorphisms
 homomorphsim->homomorphism
 homomorphsims->homomorphisms
 isomorhpism->isomorphism
 isomorhpisms->isomorphisms
+isomorhpsim->isomorphism
+isomorhpsims->isomorphisms
 isomorphsim->isomorphism
 isomorphsims->isomorphisms
 monomorhpism->monomorphism
 monomorhpisms->monomorphisms
+monomorhpsim->monomorphism
+monomorhpsims->monomorphisms
 monomorphsim->monomorphism
 monomorphsims->monomorphisms
 morhpism->morphism
 morhpisms->morphisms
+morhpsim->morphism
+morhpsims->morphisms
 morphsim->morphism
 morphsims->morphisms
 outout->output

references.bib

@@ -659,6 +659,15 @@ @phdthesis{Qui16
   langid        = {english},
 }
 
+@online{Rezk10HomotopyToposes,
+  title         = {Toposes and homotopy toposes},
+  author        = {Rezk, Charles},
+  year          = 2010,
+  month         = {01},
+  url           = {https://rezk.web.illinois.edu/homotopy-topos-sketch.pdf},
+  version       = {0.15},
+}
+
 @book{Rie17,
   title         = {Category {{Theory}} in {{Context}}},
   author        = {Riehl, Emily},

src/foundation-core/fibers-of-maps.lagda.md

@@ -52,6 +52,13 @@ module _
 
   compute-value-inclusion-fiber : (y : fiber f b) → f (inclusion-fiber y) ＝ b
   compute-value-inclusion-fiber = pr2
+
+  inclusion-fiber' : fiber' f b → A
+  inclusion-fiber' = pr1
+
+  compute-value-inclusion-fiber' :
+    (y : fiber' f b) → b ＝ f (inclusion-fiber' y)
+  compute-value-inclusion-fiber' = pr2
 ```
 
 ## Properties
@@ -280,9 +287,7 @@ module _
   triangle-map-equiv-total-fiber t = inv (pr2 (pr2 t))
 
   map-inv-equiv-total-fiber : A → Σ B (fiber f)
-  pr1 (map-inv-equiv-total-fiber x) = f x
-  pr1 (pr2 (map-inv-equiv-total-fiber x)) = x
-  pr2 (pr2 (map-inv-equiv-total-fiber x)) = refl
+  map-inv-equiv-total-fiber x = (f x , x , refl)
 
   is-retraction-map-inv-equiv-total-fiber :
     is-retraction map-equiv-total-fiber map-inv-equiv-total-fiber
@@ -316,6 +321,51 @@ module _
   pr2 inv-equiv-total-fiber = is-equiv-map-inv-equiv-total-fiber
 ```
 
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  map-equiv-total-fiber' : Σ B (fiber' f) → A
+  map-equiv-total-fiber' t = pr1 (pr2 t)
+
+  triangle-map-equiv-total-fiber' : pr1 ~ f ∘ map-equiv-total-fiber'
+  triangle-map-equiv-total-fiber' t = pr2 (pr2 t)
+
+  map-inv-equiv-total-fiber' : A → Σ B (fiber' f)
+  map-inv-equiv-total-fiber' x = (f x , x , refl)
+
+  is-retraction-map-inv-equiv-total-fiber' :
+    is-retraction map-equiv-total-fiber' map-inv-equiv-total-fiber'
+  is-retraction-map-inv-equiv-total-fiber' (.(f x) , x , refl) = refl
+
+  is-section-map-inv-equiv-total-fiber' :
+    is-section map-equiv-total-fiber' map-inv-equiv-total-fiber'
+  is-section-map-inv-equiv-total-fiber' x = refl
+
+  is-equiv-map-equiv-total-fiber' : is-equiv map-equiv-total-fiber'
+  is-equiv-map-equiv-total-fiber' =
+    is-equiv-is-invertible
+      map-inv-equiv-total-fiber'
+      is-section-map-inv-equiv-total-fiber'
+      is-retraction-map-inv-equiv-total-fiber'
+
+  is-equiv-map-inv-equiv-total-fiber' : is-equiv map-inv-equiv-total-fiber'
+  is-equiv-map-inv-equiv-total-fiber' =
+    is-equiv-is-invertible
+      map-equiv-total-fiber'
+      is-retraction-map-inv-equiv-total-fiber'
+      is-section-map-inv-equiv-total-fiber'
+
+  equiv-total-fiber' : Σ B (fiber' f) ≃ A
+  pr1 equiv-total-fiber' = map-equiv-total-fiber'
+  pr2 equiv-total-fiber' = is-equiv-map-equiv-total-fiber'
+
+  inv-equiv-total-fiber' : A ≃ Σ B (fiber' f)
+  pr1 inv-equiv-total-fiber' = map-inv-equiv-total-fiber'
+  pr2 inv-equiv-total-fiber' = is-equiv-map-inv-equiv-total-fiber'
+```
+
 ### Fibers of compositions
 
 ```agda

src/foundation-core/pullbacks.lagda.md

@@ -309,6 +309,86 @@ the vertical maps is a family of equivalences
               f
 ```
 
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
+  (f : A → X) (g : B → X) (c : cone f g C)
+  where
+
+  triangle-tot-map-fiber-vertical-map-cone' :
+    tot (map-fiber-vertical-map-cone' f g c) ~
+    gap f g c ∘ map-equiv-total-fiber' (vertical-map-cone f g c)
+  triangle-tot-map-fiber-vertical-map-cone'
+    (.(vertical-map-cone f g c x) , x , refl) = refl
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' :
+      is-pullback f g c →
+      is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb =
+      is-fiberwise-equiv-is-equiv-tot
+        ( is-equiv-left-map-triangle
+          ( tot (map-fiber-vertical-map-cone' f g c))
+          ( gap f g c)
+          ( map-equiv-total-fiber' (vertical-map-cone f g c))
+          ( triangle-tot-map-fiber-vertical-map-cone')
+          ( is-equiv-map-equiv-total-fiber' (vertical-map-cone f g c))
+          ( pb))
+
+  fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' :
+      is-pullback f g c → (x : A) →
+      fiber' (vertical-map-cone f g c) x ≃ fiber' g (f x)
+  fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb x =
+    ( map-fiber-vertical-map-cone' f g c x ,
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb x)
+
+  equiv-tot-map-fiber-vertical-map-cone-is-pullback' :
+      is-pullback f g c →
+      Σ A (fiber' (vertical-map-cone f g c)) ≃ Σ A (fiber' g ∘ f)
+  equiv-tot-map-fiber-vertical-map-cone-is-pullback' pb =
+    equiv-tot (fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb)
+
+  abstract
+    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone' :
+      is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c) →
+      is-pullback f g c
+    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone' is-equiv-fsq =
+      is-equiv-right-map-triangle
+        ( tot (map-fiber-vertical-map-cone' f g c))
+        ( gap f g c)
+        ( map-equiv-total-fiber' (vertical-map-cone f g c))
+        ( triangle-tot-map-fiber-vertical-map-cone')
+        ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq)
+        ( is-equiv-map-equiv-total-fiber' (vertical-map-cone f g c))
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' :
+      universal-property-pullback f g c →
+      is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+      up =
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback'
+        ( is-pullback-universal-property-pullback f g c up)
+
+  fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' :
+      universal-property-pullback f g c → (x : A) →
+      fiber' (vertical-map-cone f g c) x ≃ fiber' g (f x)
+  fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+    pb x =
+    ( map-fiber-vertical-map-cone' f g c x ,
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+        ( pb)
+        ( x))
+
+  equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' :
+      universal-property-pullback f g c →
+      Σ A (fiber' (vertical-map-cone f g c)) ≃ Σ A (fiber' g ∘ f)
+  equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' pb =
+    equiv-tot
+      ( fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+        ( pb))
+```
+
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
@@ -356,6 +436,15 @@ module _
           ( λ x →
             is-equiv-tot-is-fiberwise-equiv (λ y → is-equiv-inv (g y) (f x))))
         ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq)
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback :
+      universal-property-pullback f g c →
+      is-fiberwise-equiv (map-fiber-vertical-map-cone f g c)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback
+      up =
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
+        ( is-pullback-universal-property-pullback f g c up)
 ```
 
 ### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the horizontal maps

src/foundation/equivalences-arrows.lagda.md

@@ -87,8 +87,7 @@ module _
     coherence-hom-arrow f g (map-equiv i) (map-equiv j)
 
   equiv-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  equiv-arrow =
-    Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i))
+  equiv-arrow = Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i))
 
   module _
     (e : equiv-arrow)
@@ -100,6 +99,9 @@ module _
     map-domain-equiv-arrow : A → X
     map-domain-equiv-arrow = map-equiv equiv-domain-equiv-arrow
 
+    map-inv-domain-equiv-arrow : X → A
+    map-inv-domain-equiv-arrow = map-inv-equiv equiv-domain-equiv-arrow
+
     is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow
     is-equiv-map-domain-equiv-arrow =
       is-equiv-map-equiv equiv-domain-equiv-arrow
@@ -110,6 +112,9 @@ module _
     map-codomain-equiv-arrow : B → Y
     map-codomain-equiv-arrow = map-equiv equiv-codomain-equiv-arrow
 
+    map-inv-codomain-equiv-arrow : Y → B
+    map-inv-codomain-equiv-arrow = map-inv-equiv equiv-codomain-equiv-arrow
+
     is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow
     is-equiv-map-codomain-equiv-arrow =
       is-equiv-map-equiv equiv-codomain-equiv-arrow

src/foundation/fibers-of-maps.lagda.md

@@ -141,6 +141,45 @@ module _
     {y y' : B} (p : y ＝ y') (u : fiber f y) →
     tot (λ x → concat' _ p) u ＝ tr (fiber f) p u
   compute-tr-fiber refl u = ap (pair _) right-unit
+
+  inv-compute-tr-fiber :
+    {y y' : B} (p : y ＝ y') (u : fiber f y) →
+    tr (fiber f) p u ＝ tot (λ x → concat' _ p) u
+  inv-compute-tr-fiber p u = inv (compute-tr-fiber p u)
+
+  compute-tr-fiber' :
+    {y y' : B} (p : y ＝ y') (u : fiber' f y) →
+    tot (λ x q → inv p ∙ q) u ＝ tr (fiber' f) p u
+  compute-tr-fiber' refl u = refl
+
+  inv-compute-tr-fiber' :
+    {y y' : B} (p : y ＝ y') (u : fiber' f y) →
+    tr (fiber' f) p u ＝ tot (λ x q → inv p ∙ q) u
+  inv-compute-tr-fiber' p u = inv (compute-tr-fiber' p u)
+```
+
+### Transport in fibers along the fiber
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  compute-tr-self-fiber :
+    {y : B} (u : fiber f y) → (pr1 u , refl) ＝ tr (fiber f) (inv (pr2 u)) u
+  compute-tr-self-fiber (._ , refl) = refl
+
+  inv-compute-tr-self-fiber :
+    {y : B} (u : fiber f y) → tr (fiber f) (inv (pr2 u)) u ＝ (pr1 u , refl)
+  inv-compute-tr-self-fiber u = inv (compute-tr-self-fiber u)
+
+  compute-tr-self-fiber' :
+    {y : B} (u : fiber' f y) → (pr1 u , refl) ＝ tr (fiber' f) (pr2 u) u
+  compute-tr-self-fiber' (._ , refl) = refl
+
+  inv-compute-tr-self-fiber' :
+    {y : B} (u : fiber' f y) → tr (fiber' f) (pr2 u) u ＝ (pr1 u , refl)
+  inv-compute-tr-self-fiber' u = inv (compute-tr-self-fiber' u)
 ```
 
 ## Table of files about fibers of maps