Skip to content
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

Logic #1226

Merged
merged 36 commits into from
Jan 7, 2025
Merged

Logic #1226

Changes from 1 commit
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
2e74fc3
logic
fredrik-bakke Nov 18, 2024
81ace90
a word
fredrik-bakke Nov 18, 2024
e755cb0
fix import
fredrik-bakke Nov 18, 2024
2e78a1e
fixes
fredrik-bakke Nov 18, 2024
ad02d78
add references
fredrik-bakke Nov 18, 2024
ed10ff8
finitary de morgan's law
fredrik-bakke Nov 18, 2024
9f89345
fix links
fredrik-bakke Nov 18, 2024
18f72e6
fix more links
fredrik-bakke Nov 18, 2024
6abc49b
path-split type families
fredrik-bakke Nov 19, 2024
e2268d7
Merge branch 'master' into logic
fredrik-bakke Nov 21, 2024
10ea509
pre-commit
fredrik-bakke Nov 21, 2024
c043747
fix pi-finite types
fredrik-bakke Nov 21, 2024
c8237da
more logic
fredrik-bakke Nov 21, 2024
f0555c4
remove redundant formalization
fredrik-bakke Nov 21, 2024
b7a662b
pre-commit
fredrik-bakke Nov 21, 2024
1cd924a
remove hanging link
fredrik-bakke Nov 28, 2024
3d6cd60
an edit
fredrik-bakke Dec 3, 2024
3565e51
Merge branch 'master' into logic
fredrik-bakke Dec 4, 2024
f5d5404
edits foundation
fredrik-bakke Dec 8, 2024
0594fe7
suspensions of propositions
fredrik-bakke Dec 9, 2024
d5bbcb6
ac => lem
fredrik-bakke Dec 9, 2024
c6c4320
informal proof diaconescu
fredrik-bakke Dec 9, 2024
69b5e09
formatting suspensions of propositions
fredrik-bakke Dec 9, 2024
da33f20
fix links
fredrik-bakke Dec 9, 2024
e87ff8f
Merge branch 'master' into logic
fredrik-bakke Jan 6, 2025
d152b94
a little bit of self-review
fredrik-bakke Jan 6, 2025
7350dd7
fix an entry name
fredrik-bakke Jan 6, 2025
ed07ea7
remove a pair of quotation marks
fredrik-bakke Jan 6, 2025
a3201b0
factor out markovian types and other edits
fredrik-bakke Jan 6, 2025
879a132
Merge branch 'master' into logic
fredrik-bakke Jan 6, 2025
6c29f54
pre-commit
fredrik-bakke Jan 6, 2025
9ac3d57
review
fredrik-bakke Jan 7, 2025
1abc3ed
pre-commit
fredrik-bakke Jan 7, 2025
4f8b9c6
Merge branch 'master' into logic
fredrik-bakke Jan 7, 2025
efaaa3a
add module `foundation.uniformly-decidable-type-families`
fredrik-bakke Jan 7, 2025
0409770
fix link
fredrik-bakke Jan 7, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
pre-commit
fredrik-bakke committed Nov 21, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 10ea50914fd505f3d23031bce23c6245fae4b0d7
1 change: 1 addition & 0 deletions src/foundation.lagda.md
Original file line number Diff line number Diff line change
@@ -302,6 +302,7 @@ open import foundation.partitions public
open import foundation.path-algebra public
open import foundation.path-cosplit-maps public
open import foundation.path-split-maps public
open import foundation.path-split-type-families public
open import foundation.perfect-images public
open import foundation.permutations-spans-families-of-types public
open import foundation.pi-decompositions public
2 changes: 1 addition & 1 deletion src/foundation/double-negation-modality.lagda.md
Original file line number Diff line number Diff line change
@@ -20,7 +20,7 @@ open import foundation-core.function-types
open import foundation-core.transport-along-identifications

open import logic.double-negation-elimination

open import orthogonal-factorization-systems.continuation-modalities
open import orthogonal-factorization-systems.large-lawvere-tierney-topologies
open import orthogonal-factorization-systems.lawvere-tierney-topologies
11 changes: 5 additions & 6 deletions src/foundation/path-split-type-families.lagda.md
Original file line number Diff line number Diff line change
@@ -7,20 +7,20 @@ module foundation.path-split-type-families where
<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.transport-along-identifications
open import foundation.action-on-identifications-functions
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.sections
open import foundation-core.subtypes
open import foundation.embeddings
open import foundation-core.equality-dependent-pair-types
open import foundation-core.dependent-identifications
open import foundation-core.equality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.sections
open import foundation-core.subtypes
```

</details>
@@ -88,7 +88,6 @@ module _
(H : is-path-split-family P)
where


all-elements-equal-is-path-split-family : {x : A} (u v : P x) → u = v
all-elements-equal-is-path-split-family u v = H refl u v

Original file line number Diff line number Diff line change
@@ -10,9 +10,9 @@ module modal-type-theory.transport-along-crisp-identifications where

```agda
open import foundation.action-on-identifications-functions
open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels
open import foundation.function-types

open import modal-type-theory.crisp-identity-types
```