prove SETᴰ is a fibration, re-org SETᴰ

maxsnew · Mar 7, 2024 · bf262c1 · bf262c1
1 parent efef128
commit bf262c1
Show file tree

Hide file tree

Showing 4 changed files with 42 additions and 3 deletions.
diff --git a/Cubical/Categories/Displayed/Adjoint/More.agda b/Cubical/Categories/Displayed/Adjoint/More.agda
@@ -12,7 +12,7 @@ open import Cubical.Categories.Adjoint.UniversalElements
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Base.More
 open import Cubical.Categories.Displayed.Functor
-open import Cubical.Categories.Displayed.Instances.Sets
+open import Cubical.Categories.Displayed.Instances.Sets.Base
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Displayed.Presheaf
 open import Cubical.Categories.Presheaf.Representable

diff --git a/.../Categories/Displayed/Instances/Sets.agda → ...gories/Displayed/Instances/Sets/Base.agda b/.../Categories/Displayed/Instances/Sets.agda → ...gories/Displayed/Instances/Sets/Base.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Cubical.Categories.Displayed.Instances.Sets where
+module Cubical.Categories.Displayed.Instances.Sets.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function

diff --git a/Cubical/Categories/Displayed/Instances/Sets/Properties.agda b/Cubical/Categories/Displayed/Instances/Sets/Properties.agda
@@ -0,0 +1,39 @@
+{-# OPTIONS --safe --lossy-unification #-}
+module Cubical.Categories.Displayed.Instances.Sets.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Structure
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sigma.Properties
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Base.More
+open import Cubical.Categories.Displayed.Functor
+open import Cubical.Categories.Displayed.Fibration
+open import Cubical.Categories.Displayed.Instances.Sets.Base
+open import Cubical.Categories.Displayed.Presheaf
+
+private
+  variable
+    ℓ ℓ' ℓ'' ℓ''' : Level
+    ℓC ℓC' ℓD ℓD' : Level
+
+open UniversalElementᴰ
+open CartesianOver
+open Categoryᴰ
+
+AllCartesianOversSETᴰ : AllCartesianOvers (SETᴰ ℓ ℓ')
+AllCartesianOversSETᴰ {A} {A'} B' f .f*cᴰ' x = B' (f x)
+AllCartesianOversSETᴰ {A} {A'} B' f .π a b'  = b'
+AllCartesianOversSETᴰ {A} {A'} B' f .isCartesian B'' g gfᴰ =
+  uniqueExists gfᴰ refl ((λ _ → SETᴰ _ _ .isSetHomᴰ _ _))
+    λ gfᴰ' → sym
+
+isFibrationSet : isFibration (SETᴰ ℓ ℓ')
+isFibrationSet dᴰ = CartesianOver→CartesianLift (SETᴰ _ _)
+  (AllCartesianOversSETᴰ (dᴰ .fst .snd) (dᴰ .snd))
diff --git a/Cubical/Categories/Displayed/Presheaf.agda b/Cubical/Categories/Displayed/Presheaf.agda
@@ -16,7 +16,7 @@ open import Cubical.Categories.Presheaf.Representable
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Base.More
-open import Cubical.Categories.Displayed.Instances.Sets
+open import Cubical.Categories.Displayed.Instances.Sets.Base
 open import Cubical.Categories.Displayed.Functor
 
 private