Skip to content

Make join-assoc level-polymorphic #1204

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

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Make join-assoc level-polymorphic #1204

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
78cff13
Add level polymorphism
ricky136973 May 5, 2025
6c8f25f
Generalize level polymorphism
ricky136973 May 20, 2025
6852366
Merge remote-tracking branch 'upstream/master' into join-assoc-level-…
ricky136973 May 20, 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
44 changes: 40 additions & 4 deletions Cubical/HITs/Join/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ module Cubical.HITs.Join.Properties where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
Expand Down Expand Up @@ -99,8 +100,8 @@ joinPushout≡join A B = isoToPath (joinPushout-iso-join A B)
{-
Proof of associativity of the join
-}
join-assoc : (A B C : Type₀) → join (join A B) C ≡ join A (join B C)
join-assoc A B C = (joinPushout≡join (join A B) C) ⁻¹
join-assoc-samelevel : (A B C : Type ℓ) → join (join A B) C ≡ join A (join B C)
join-assoc-samelevel {ℓ} A B C = (joinPushout≡join (join A B) C) ⁻¹
∙ (spanEquivToPushoutPath sp3≃sp4) ⁻¹
∙ (3x3-span.3x3-lemma span) ⁻¹
∙ (spanEquivToPushoutPath sp1≃sp2)
Expand Down Expand Up @@ -163,7 +164,7 @@ join-assoc A B C = (joinPushout≡join (join A B) C) ⁻¹
H1 = H1;
H3 = H2 }
where
A×join : Type₀
A×join : Type ℓ
A×join = A × (join B C)

A□2→A×join : 3x3-span.A□2 span → A×join
Expand Down Expand Up @@ -245,7 +246,7 @@ join-assoc A B C = (joinPushout≡join (join A B) C) ⁻¹
H1 = H4;
H3 = H3 }
where
join×C : Type₀
join×C : Type ℓ
join×C = (join A B) × C

A2□→join×C : 3x3-span.A2□ span → join×C
Expand Down Expand Up @@ -300,6 +301,41 @@ join-assoc A B C = (joinPushout≡join (join A B) C) ⁻¹
H4 (inr (b , c)) = refl
H4 (push (a , (b , c)) i) j = fst (joinPushout≃join _ _) (doubleCompPath-filler refl (λ i → push (a , b) i) refl j i)

join-assoc : ∀ {ℓ''} (A : Type ℓ) (B : Type ℓ') (C : Type ℓ'') → join (join A B) C ≡ join A (join B C)
join-assoc {ℓ} {ℓ'} {ℓ''} A B C =
LiftExt {ℓ' = ℓ-max (ℓ-max ℓ ℓ') ℓ''} (join-lift ⁻¹
∙ cong₂ join join-lift refl ⁻¹
∙ join-assoc-samelevel (Lift A) (Lift B) (Lift C)
∙ cong₂ join refl join-lift
∙ join-lift)
where
join-lift : ∀ {ℓ ℓ' ℓ-out} {A : Type ℓ} {B : Type ℓ'} →
join (Lift {j = ℓ-out} A) (Lift {j = ℓ-out} B) ≡ Lift {j = ℓ-out} (join A B)
join-lift {ℓ-out = ℓ-out} {A = A} {B = B} = isoToPath (iso f g fg gf)
where
f : join (Lift {j = ℓ-out} A) (Lift {j = ℓ-out} B) → Lift {j = ℓ-out} (join A B)
f (inl (lift x)) = lift (inl x)
f (inr (lift x)) = lift (inr x)
f (push (lift a) (lift b) i) = lift (push a b i)

g : Lift {j = ℓ-out} (join A B) → join (Lift {j = ℓ-out} A) (Lift {j = ℓ-out} B)
g (lift (inl x)) = inl (lift x)
g (lift (inr x)) = inr (lift x)
g (lift (push a b i)) = push (lift a) (lift b) i

fg : ∀ x → f (g x) ≡ x
fg (lift (inl x)) = refl
fg (lift (inr x)) = refl
fg (lift (push a b i)) = refl

gf : ∀ x → g (f x) ≡ x
gf (inl (lift x)) = refl
gf (inr (lift x)) = refl
gf (push (lift a) (lift b) i) = refl

LiftExt : ∀ {ℓ ℓ'} {A B : Type ℓ} → Lift {j = ℓ'} A ≡ Lift {j = ℓ'} B → A ≡ B
LiftExt p = ua (LiftEquiv ∙ₑ pathToEquiv p ∙ₑ invEquiv LiftEquiv)

{-
Direct proof of an associativity-related property. Combined with
commutativity, this implies that the join is associative.
Expand Down