-
Notifications
You must be signed in to change notification settings - Fork 63
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Project: Sheaves and excision with respect to regular cd-structures #930
Comments
I've already defined the closed modality. It's in |
This PR sets up some initial definitions for #930.
Cartesian morphisms of arrows were added in #979. |
This issue seems to be missing any mention of orthogonal maps or fiberwise orthogonal maps. Are they not needed? |
When you write
Are you looking for a file about the following construct? base-change-arrow :
{l1 l2 : Level} (l3 l4 : Level) {A : UU l1} {B : UU l2} → (A → B) →
UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4)
base-change-arrow l3 l4 f =
Σ (UU l3) (λ C → Σ (UU l4) (λ D → Σ (C → D) (λ g → cartesian-hom-arrow g f))) Otherwise, just using cartesian morphisms of arrows seems to be working fine with me for now. Although I would probably say the same about cartesian morphisms of arrows vs. pullback cones if we didn't already have cartesian morphisms of arrows. EDIT: Oh, wait, you want a base change of morphisms of arrows. |
Defines `Y`-null maps, `Y`-null types and `Y`-null type families, and establishes a few basic properties of these. Also formalizes the fiber condition for orthogonal maps. Part of #930. Depends on #1086. - If `A` is a retract of `B` and `S` is a retract of `T` then `diagonal-exponential A S` is a retract of `diagonal-exponential B T`. - Null types - Null types are closed under equivalences in the base and exponent - Null types are closed under retracts in the base and exponent - A type is `Y`-null if and only if the terminal projection of `Y` is orthogonal to the terminal projection of `A` - Null families - Null families are closed under equivalences in the family and exponent - Null families are closed under retracts in the family and exponent - Null maps, equivalence of - Fiber condition - Pullback condition - Right orthogonal map to terminal projection condition - Local at terminal projection condition - Fiber condition for orthogonal maps
The cd-excision project
Project description
A complete cd-structure consists of a class of distinguished squares of maps, i.e., distinguished morphisms in the arrow category, that is stable under base change. A complete cd-structure is said to be regular if the following three conditions hold:
A type
F
is said to be a sheaf with respect to a cd-structure ifF
is right orthogonal toinclusion-im (cogap d)
for any distinguished squared
.A type
F
is said to satisfy excision with respect to a cd-structure ifF
is right orthogonal tocogap d
for any distinguished squared
.Goal of the project: Show that
F
is a sheaf with respect to a regular cd-structure if and only if it satisfies excision.Current participants: Reid Barton, Egbert Rijke, Fredrik Bakke.
Outline and tasks
Descent
The closed modality
The arrow category
pullback-squares
for real-world applications, and possibly rename it tocartesian squares
. Alternatively, introduce a file for cartesian morphisms of arrows.Wärn's first lemma
Orthogonality
Π
, left orthogonal maps underΣ
Given a jointly surjective family of maps
f
-local types (what is called fiberwise orthogonal in the notes)Cd-structures
Resources
The text was updated successfully, but these errors were encountered: