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.

Sign up for GitHub

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

Induction principle for smash product #1098

Merged
merged 17 commits into from
Feb 5, 2024
Merged

Induction principle for smash product #1098

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
93d7248
t
aljungstrom Feb 1, 2022
b4b6efb
m
aljungstrom Feb 1, 2022
cc6ced2
done
aljungstrom Apr 24, 2023
e8244ac
duplicate
aljungstrom Apr 24, 2023
aadde33
wups
aljungstrom Apr 24, 2023
17f3fc1
rme
aljungstrom Apr 24, 2023
9341710
ganea stuff
aljungstrom Jun 2, 2023
52429ff
Merge branch 'newM'
aljungstrom Jun 8, 2023
ea75092
w
aljungstrom Jun 8, 2023
3acc6b8
w
aljungstrom Jun 8, 2023
227b10b
w
aljungstrom Jun 8, 2023
f4745a2
Merge remote-tracking branch 'origin/master'
aljungstrom Jan 31, 2024
58c6104
placeholder
aljungstrom Jan 31, 2024
bf1bf40
done
aljungstrom Feb 3, 2024
e29b1c3
merge
aljungstrom Feb 3, 2024
6475e57
renaming
aljungstrom Feb 4, 2024
2d7b8ce
typo
aljungstrom Feb 5, 2024
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
2 changes: 1 addition & 1 deletion Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.Equiv

open import Cubical.Data.Nat
open import Cubical.Data.Fin
open import Cubical.Data.Fin hiding (FinVec)
open import Cubical.Data.Fin.Arithmetic
open import Cubical.Data.FinData
open import Cubical.Data.Vec
Expand Down
2 changes: 1 addition & 1 deletion Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ open import Cubical.Cohomology.EilenbergMacLane.Rings.Z2-properties
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Unit
open import Cubical.Data.Fin
open import Cubical.Data.Fin hiding (FinVec)
open import Cubical.Data.Fin.Arithmetic
open import Cubical.Data.Sigma
open import Cubical.Data.Vec
Expand Down
30 changes: 30 additions & 0 deletions Cubical/Data/Fin/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ module Cubical.Data.Fin.Base where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Pointed

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat using (ℕ ; zero ; suc ; _+_ ; znots)
Expand Down Expand Up @@ -44,6 +45,9 @@ fzero≠fone p = znots (cong fst p)
fsuc : Fin k → Fin (suc k)
fsuc (k , l) = (suc k , suc-≤-suc l)

finj : Fin k → Fin (suc k)
finj (k , l) = k , ≤-trans l (1 , refl)

-- Conversion back to ℕ is trivial...
toℕ : Fin k → ℕ
toℕ = fst
Expand Down Expand Up @@ -109,3 +113,29 @@ FinPathℕ : {n : ℕ} (x : Fin n) (y : ℕ) → fst x ≡ y → Σ[ p ∈ _ ] (
FinPathℕ {n = n} x y p =
((fst (snd x)) , (cong (λ y → fst (snd x) + y) (cong suc (sym p)) ∙ snd (snd x)))
, (Σ≡Prop (λ _ → isProp≤) p)

FinVec : (A : Type ℓ) (n : ℕ) → Type ℓ
FinVec A n = Fin n → A
mortberg marked this conversation as resolved.
Show resolved Hide resolved

FinFamily : (n : ℕ) (ℓ : Level) → Type (ℓ-suc ℓ)
FinFamily n ℓ = FinVec (Type ℓ) n

FinFamily∙ : (n : ℕ) (ℓ : Level) → Type (ℓ-suc ℓ)
FinFamily∙ n ℓ = FinVec (Pointed ℓ) n

predFinFamily : {n : ℕ} → FinFamily (suc n) ℓ → FinFamily n ℓ
predFinFamily A n = A (finj n)

predFinFamily∙ : {n : ℕ} → FinFamily∙ (suc n) ℓ → FinFamily∙ n ℓ
fst (predFinFamily∙ A x) = predFinFamily (fst ∘ A) x
snd (predFinFamily∙ A x) = snd (A _)

prodFinFamily : (n : ℕ) → FinFamily (suc n) ℓ → Type ℓ
prodFinFamily zero A = A fzero
prodFinFamily (suc n) A = prodFinFamily n (predFinFamily A) × A flast

prodFinFamily∙ : (n : ℕ) → FinFamily∙ (suc n) ℓ → Pointed ℓ
fst (prodFinFamily∙ n A) = prodFinFamily n (fst ∘ A)
snd (prodFinFamily∙ zero A) = snd (A fzero)
snd (prodFinFamily∙ (suc n) A) =
snd (prodFinFamily∙ n (predFinFamily∙ A)) , snd (A flast)
2 changes: 1 addition & 1 deletion Cubical/HITs/SmashProduct.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
module Cubical.HITs.SmashProduct where

open import Cubical.HITs.SmashProduct.Base public

open import Cubical.HITs.SmashProduct.Induction public
-- open import Cubical.HITs.SmashProduct.Properties public
Loading
Loading