Skip to content

Make Lift's level argument explicit #1273

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
anshwad10 wants to merge 12 commits into
base: master
Choose a base branch
from
Open

Make Lift's level argument explicit #1273

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
2c08d38
make lift take explicit level argument
anshwad10 Nov 15, 2025
d0a016f
Merge branch 'explicit-lift' of https://github.com/anshwad10/cubical …
anshwad10 Nov 15, 2025
c26b5c4
chore: make level arguments explicit pt 1
anshwad10 Nov 15, 2025
577c2f8
chore: make level arguments explicit pt 2
anshwad10 Nov 15, 2025
93d75cd
chore: make level arguments explicit pt 3
anshwad10 Nov 15, 2025
f14a674
chore: make level arguments explicit pt 3
anshwad10 Nov 15, 2025
6090714
chore: make level arguments explicit pt 4
anshwad10 Nov 15, 2025
19538f0
chore: make level arguments explicit pt 4
anshwad10 Nov 15, 2025
be19720
rename liftMap
anshwad10 Nov 15, 2025
3e31d6c
i think this is the last one
anshwad10 Nov 15, 2025
d114d6a
this better be the last one
anshwad10 Nov 15, 2025
61af5bd
now this has got be the last one
anshwad10 Nov 15, 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
4 changes: 2 additions & 2 deletions Cubical/Axiom/UniquenessOfIdentity.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,8 @@ module _ {A : Type ℓ} where
¬UIPType {ℓ} uip =
false≢true (cong lower (transport-uip p (lift true)))
where
B = Lift {j = ℓ} Bool
p = cong (Lift {j = ℓ}) (ua notEquiv)
B = Bool*
p = cong (Lift ℓ) (ua notEquiv)

transport-uip : (p : B ≡ B) → ∀ b → transport p b ≡ b
transport-uip = UIP→AxiomK uip _ B _ transportRefl
45 changes: 17 additions & 28 deletions Cubical/CW/Connected.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -583,38 +583,27 @@ module _ (A : ℕ → Type ℓ) (sk+c : yieldsCombinatorialConnectedCWskel A 0)
collapse₁card (suc (suc x)) = AC.card (suc (suc x))

collapse₁CWskel : ℕ → Type _
collapse₁CWskel zero = Lift ⊥
collapse₁CWskel (suc zero) = Lift (Fin 1)
collapse₁CWskel zero = ⊥*
collapse₁CWskel (suc zero) = Unit*
collapse₁CWskel (suc (suc n)) = A (suc (suc n))

collapse₁α : (n : ℕ)
→ Fin (collapse₁card n) × S⁻ n → collapse₁CWskel n
collapse₁α (suc zero) (x , p) = lift fzero
collapse₁α (suc zero) (x , p) = tt*
collapse₁α (suc (suc n)) = AC.α (2 +ℕ n)

connectedCWskel→ : yieldsConnectedCWskel collapse₁CWskel 0
fst (fst connectedCWskel→) = collapse₁card
fst (snd (fst connectedCWskel→)) = collapse₁α
fst (snd (snd (fst connectedCWskel→))) = λ()
snd (snd (snd (fst connectedCWskel→))) zero =
isContr→Equiv (isOfHLevelLift 0 (inhProp→isContr fzero isPropFin1))
((inr fzero)
, (λ { (inr x) j → inr (isPropFin1 fzero x j) }))
snd (snd (snd (fst connectedCWskel→))) (suc zero) =
compEquiv (invEquiv (isoToEquiv e₁))
(compEquiv (isoToEquiv (snd liftStr))
(isoToEquiv (pushoutIso _ _ _ _
(idEquiv _) LiftEquiv (idEquiv _)
(funExt cohₗ) (funExt cohᵣ))))
where
-- Agda complains if these proofs are inlined...
cohₗ : (x : _) → collapse₁α 1 x ≡ collapse₁α 1 x
cohₗ (x , p) = refl

cohᵣ : (x : Fin (fst liftStr) × Bool) → fst x ≡ fst x
cohᵣ x = refl
snd (snd (snd (fst connectedCWskel→))) (suc (suc n)) = AC.e (suc (suc n))
snd connectedCWskel→ = refl , (λ _ → λ ())
connectedCWskel→ .fst .fst = collapse₁card
connectedCWskel→ .fst .snd .fst = collapse₁α
connectedCWskel→ .fst .snd .snd .fst ()
connectedCWskel→ .fst .snd .snd .snd zero = isContr→Equiv isContrUnit* (inr fzero , λ { (inr x) → cong inr (isPropFin1 fzero x) })
connectedCWskel→ .fst .snd .snd .snd (suc zero) = isoToEquiv $
A 2 Iso⟨ invIso e₁ ⟩
Pushout (CW₁-discrete (A , sk) .fst ∘ AC.α 1) fst Iso⟨ liftStr .snd ⟩
Pushout (λ _ → fzero) fst Iso⟨ pushoutIso _ _ _ _ (idEquiv _) (isContr→≃Unit* isContrFin1) (idEquiv _) refl refl ⟩
Pushout (collapse₁α 1) fst ∎Iso
connectedCWskel→ .fst .snd .snd .snd (suc (suc n)) = AC.e (suc (suc n))
connectedCWskel→ .snd = refl , λ _ ()

collapse₁Equiv : (n : ℕ)
→ realise (_ , sk) ≃ realise (_ , connectedCWskel→ .fst)
Expand Down Expand Up @@ -1221,7 +1210,7 @@ makeConnectedCW {ℓ = ℓ} (suc n) {C = C} (cwsk , eqv) cA with
C' zero (lt x) = ⊥*
C' (suc m) (lt x) = Unit*
C' m (eq x) =
Lift (SphereBouquet 2+n (A 2+n))
Lift _ (SphereBouquet 2+n (A 2+n))
C' m (gt x) = C* m

-- Basepoints (not needed, but useful)
Expand Down Expand Up @@ -1364,7 +1353,7 @@ connectedCWContr : {ℓ : Level} (n m : ℕ) (l : m <ᵗ suc n) (X : Type ℓ)
(cwX : isConnectedCW n X) → isContr (fst (fst cwX) (suc m))
connectedCWContr n zero l X cwX =
subst isContr
(cong (Lift ∘ Fin) (sym ((snd (fst cwX)) .snd .fst))
(cong (Lift _ ∘ Fin) (sym ((snd (fst cwX)) .snd .fst))
∙ sym (ua (compEquiv (CW₁-discrete (connectedCWskel→CWskel (fst cwX)))
LiftEquiv)))
(isOfHLevelLift 0 (inhProp→isContr fzero isPropFin1))
Expand Down Expand Up @@ -1515,7 +1504,7 @@ module isFinitelyPresented-π'connectedCW-lemmas {ℓ : Level}
lem : (α : FinSphereBouquetMap∙
(card Xˢᵏᵉˡ (suc (suc (suc n)))) (card Xˢᵏᵉˡ (suc (suc n)))
(suc n))
(e : fst X₄₊ₙ∙ ≡ Lift (cofib (fst α)))
(e : fst X₄₊ₙ∙ ≡ Lift _ (cofib (fst α)))
→ ∥ PathP (λ i → e (~ i)) (lift (inl tt)) x ∥₁
lem α e = TR.rec squash₁ ∣_∣₁ (isConnectedPathP _ isConX' _ _ .fst)

Expand Down
2 changes: 1 addition & 1 deletion Cubical/CW/HurewiczTheorem.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1249,7 +1249,7 @@ HurewiczTheorem n =
Xᶜʷ = X , cw
Xᶜʷ' = X , Xˢᵏᵉˡ' , (invEquiv (snd cw'))

liftLem : (A : CW ℓ-zero) (a : fst A) (e : isConnected 2 (Lift (fst A)))
liftLem : (A : CW ℓ-zero) (a : fst A) (e : isConnected 2 (Lift _ (fst A)))
→ Path (Σ[ A ∈ CW ℓ-zero ] (Σ[ a ∈ fst A ] isConnected 2 (fst A)))
(A , a , subst (isConnected 2) (ua (invEquiv LiftEquiv)) e)
((CWLift ℓ-zero A) , (lift a , e))
Expand Down
10 changes: 5 additions & 5 deletions Cubical/CW/Instances/Lift.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ private

module _ (ℓ : Level) where
CWskelLift : CWskel ℓA → CWskel (ℓ-max ℓA ℓ)
fst (CWskelLift sk) n = Lift {j = ℓ} (fst sk n)
fst (CWskelLift sk) n = Lift ℓ (fst sk n)
fst (snd (CWskelLift sk)) = CWskel-fields.card sk
fst (snd (snd (CWskelLift sk))) n (x , a) =
lift (CWskel-fields.α sk n (x , a))
Expand All @@ -33,15 +33,15 @@ module _ (ℓ : Level) where
(pushoutEquiv _ _ _ _ (idEquiv _)
LiftEquiv (idEquiv _) refl refl))

hasCWskelLift : {A : Type ℓA} → hasCWskel A → hasCWskel (Lift {j = ℓ} A)
hasCWskelLift : {A : Type ℓA} → hasCWskel A → hasCWskel (Lift ℓ A)
fst (hasCWskelLift (sk , e)) = CWskelLift sk
snd (hasCWskelLift (sk , e)) =
compEquiv (invEquiv LiftEquiv)
(compEquiv e
(invEquiv (isoToEquiv (SeqColimLift {ℓ = ℓ} _))))

CWLift : CW ℓA → CW (ℓ-max ℓA ℓ)
fst (CWLift (A , sk)) = Lift {j = ℓ} A
fst (CWLift (A , sk)) = Lift ℓ A
snd (CWLift (A , sk)) = PT.map hasCWskelLift sk

finCWskelLift : ∀ {n} → finCWskel ℓA n → finCWskel (ℓ-max ℓA ℓ) n
Expand All @@ -52,12 +52,12 @@ module _ (ℓ : Level) where
(compEquiv (_ , snd (snd sk) k) LiftEquiv) .snd

hasFinCWskelLift : {A : Type ℓA}
→ hasFinCWskel A → hasFinCWskel (Lift {j = ℓ} A)
→ hasFinCWskel A → hasFinCWskel (Lift ℓ A)
fst (hasFinCWskelLift (dim , sk , e)) = dim
fst (snd (hasFinCWskelLift (dim , sk , e))) = finCWskelLift sk
snd (snd (hasFinCWskelLift c)) =
hasCWskelLift (hasFinCWskel→hasCWskel _ c) .snd

finCWLift : finCW ℓA → finCW (ℓ-max ℓA ℓ)
fst (finCWLift (A , sk)) = Lift {j = ℓ} A
fst (finCWLift (A , sk)) = Lift ℓ A
snd (finCWLift (A , sk)) = PT.map hasFinCWskelLift sk
31 changes: 17 additions & 14 deletions Cubical/CW/Instances/Pushout.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -756,8 +756,11 @@ module _ {ℓ ℓ' : Level} (P : Type ℓ → Type ℓ') (P1 : P Unit*) (P0 : P
(Ppush : (A B C : Type ℓ) (f : A → B) (g : A → C)
→ P A → P B → P C → P (Pushout f g)) where
private
PFin1 : P (Lift (Fin 1))
PFin1 = subst P (cong Lift (isoToPath Iso-Unit-Fin1)) P1
L : Type → Type ℓ
L = Lift ℓ

PFin1 : P (L (Fin 1))
PFin1 = subst P (cong L (isoToPath Iso-Unit-Fin1)) P1

P⊎ : {B C : Type ℓ} → P B → P C → P (B ⊎ C)
P⊎ {B = B} {C} pB pC =
Expand All @@ -767,35 +770,35 @@ module _ {ℓ ℓ' : Level} (P : Type ℓ → Type ℓ') (P1 : P Unit*) (P0 : P
PushoutEmptyDomainIso))
(Ppush ⊥* B C (λ ()) (λ ()) P0 pB pC)

PFin : (n : ℕ) → P (Lift (Fin n))
PFin : (n : ℕ) → P (Lift _ (Fin n))
PFin zero =
subst P
(cong Lift
(cong L
(ua (propBiimpl→Equiv isProp⊥
(λ x → ⊥.rec (¬Fin0 x)) (λ()) ¬Fin0)))
P0
PFin (suc n) =
subst P (cong Lift (sym (isoToPath Iso-Fin-Unit⊎Fin)))
subst P (cong (Lift _) (sym (isoToPath Iso-Fin-Unit⊎Fin)))
(subst P (isoToPath (Lift⊎Iso ℓ))
(P⊎ P1 (PFin n)))

PS : (n : ℕ) → P (Lift (S⁻ n))
PS : (n : ℕ) → P (L (S⁻ n))
PS zero = P0
PS (suc zero) = subst P (cong Lift (isoToPath (invIso Iso-Bool-Fin2))) (PFin 2)
PS (suc zero) = subst P (cong L (isoToPath (invIso Iso-Bool-Fin2))) (PFin 2)
PS (suc (suc n)) =
subst P
(cong Lift (isoToPath (compIso PushoutSuspIsoSusp (invIso (IsoSucSphereSusp n)))))
(cong L (isoToPath (compIso PushoutSuspIsoSusp (invIso (IsoSucSphereSusp n)))))
(subst P (isoToPath (LiftPushoutIso ℓ))
(Ppush (Lift (S₊ n)) Unit* Unit* (λ _ → tt*) (λ _ → tt*)
(Ppush (L (S₊ n)) Unit* Unit* (λ _ → tt*) (λ _ → tt*)
(PS (suc n)) P1 P1))

PFin×S : (n m : ℕ) → P (Lift (Fin n × S⁻ m))
PFin×S : (n m : ℕ) → P (L (Fin n × S⁻ m))
PFin×S zero m =
subst P (ua (compEquiv (uninhabEquiv (λ()) λ()) LiftEquiv)) P0
subst P (ua (uninhabEquiv lower λ ())) P0
PFin×S (suc n) m = subst P (isoToPath is) (P⊎ (PS m) (PFin×S n m))
where
is : Iso (Lift (S⁻ m) ⊎ Lift (Fin n × S⁻ m))
(Lift (Fin (suc n) × S⁻ m))
is : Iso (L (S⁻ m) ⊎ L (Fin n × S⁻ m))
(L (Fin (suc n) × S⁻ m))
is =
compIso (Lift⊎Iso ℓ)
(compIso (invIso LiftIso)
Expand All @@ -815,7 +818,7 @@ module _ {ℓ ℓ' : Level} (P : Type ℓ → Type ℓ') (P1 : P Unit*) (P0 : P
refl refl)
(invEquiv (B .snd .snd .snd .snd n))))
(Ppush _ _ _
(λ { (lift r) → CWskel-fields.α B n r}) (liftFun fst)
(λ { (lift r) → CWskel-fields.α B n r}) (liftMap fst)
(PFin×S (CWskel-fields.card B n) n)
(PCWskel B n) (PFin (CWskel-fields.card B n)))

Expand Down
2 changes: 1 addition & 1 deletion Cubical/Categories/Constructions/Lift.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ open Category
module _ (C : Category ℓ ℓ') (ℓ'' : Level) where
LiftHoms : Category ℓ (ℓ-max ℓ' ℓ'')
LiftHoms .ob = C .ob
LiftHoms .Hom[_,_] A B = Lift {j = ℓ''} (C [ A , B ])
LiftHoms .Hom[_,_] A B = Lift ℓ'' (C [ A , B ])
LiftHoms .id = lift (C .id)
LiftHoms ._⋆_ f g = lift (f .lower ⋆⟨ C ⟩ g .lower)
LiftHoms .⋆IdL f = cong lift (C .⋆IdL (f .lower))
Expand Down
26 changes: 13 additions & 13 deletions Cubical/Categories/Instances/Sets.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,20 +48,20 @@ _[_,-] : (C : Category ℓ ℓ') → (c : C .ob)→ Functor C (SET ℓ')
(C [ c ,-]) .F-seq _ _ = funExt λ _ → sym (C .⋆Assoc _ _ _)

-- Lift functor
LiftF : Functor (SET ℓ) (SET (ℓ-max ℓ ℓ'))
LiftF {ℓ}{ℓ'} .F-ob A = (Lift {ℓ}{ℓ'} (A .fst)) , isOfHLevelLift 2 (A .snd)
LiftF .F-hom f x = lift (f (x .lower))
LiftF .F-id = refl
LiftF .F-seq f g = funExt λ x → refl
LiftF : ∀ ℓ' → Functor (SET ℓ) (SET (ℓ-max ℓ ℓ'))
LiftF ℓ' .F-ob A = (Lift ℓ' (A .fst)) , isOfHLevelLift 2 (A .snd)
LiftF ℓ' .F-hom f x = lift (f (x .lower))
LiftF ℓ' .F-id = refl
LiftF ℓ' .F-seq f g = funExt λ x → refl

module _ {ℓ ℓ' : Level} where
isFullyFaithfulLiftF : isFullyFaithful (LiftF {ℓ} {ℓ'})
isFullyFaithfulLiftF : isFullyFaithful (LiftF {ℓ} ℓ')
isFullyFaithfulLiftF X Y = isoToIsEquiv LiftFIso
where
open Iso
LiftFIso : Iso (X .fst → Y .fst)
(Lift {ℓ}{ℓ'} (X .fst) → Lift {ℓ}{ℓ'} (Y .fst))
fun LiftFIso = LiftF .F-hom {X} {Y}
(Lift ℓ' (X .fst) → Lift ℓ' (Y .fst))
fun LiftFIso = LiftF ℓ' .F-hom {X} {Y}
inv LiftFIso = λ f x → f (lift x) .lower
rightInv LiftFIso = λ _ → funExt λ _ → refl
leftInv LiftFIso = λ _ → funExt λ _ → refl
Expand Down Expand Up @@ -189,7 +189,7 @@ module _ {ℓ} where
-- LiftF : SET ℓ → SET (ℓ-suc ℓ) preserves "small" limits
-- i.e. limits over diagram shapes J : Category ℓ ℓ
module _ {ℓ : Level} where
preservesLimitsLiftF : preservesLimits {ℓJ = ℓ} {ℓJ' = ℓ} (LiftF {ℓ} {ℓ-suc ℓ})
preservesLimitsLiftF : preservesLimits {ℓJ = ℓ} {ℓJ' = ℓ} (LiftF {ℓ} (ℓ-suc ℓ))
preservesLimitsLiftF = preservesLimitsChar _
completeSET
completeSETSuc
Expand All @@ -209,22 +209,22 @@ module _ {ℓ : Level} where
(λ x hx → funExt (λ d → cone≡ λ u → funExt (λ _ → sym (funExt⁻ (hx u) d))))

lowerCone : ∀ J D
→ Cone (LiftF ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit)
→ Cone (LiftF _ ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit)
→ Cone D (Unit* , isOfHLevelLift 2 isSetUnit)
coneOut (lowerCone J D cc) v tt* = cc .coneOut v tt* .lower
coneOutCommutes (lowerCone J D cc) e =
funExt λ { tt* → cong lower (funExt⁻ (cc .coneOutCommutes e) tt*) }

liftCone : ∀ J D
→ Cone D (Unit* , isOfHLevelLift 2 isSetUnit)
→ Cone (LiftF ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit)
→ Cone (LiftF _ ∘F D) (Unit* , isOfHLevelLift 2 isSetUnit)
coneOut (liftCone J D cc) v tt* = lift (cc .coneOut v tt*)
coneOutCommutes (liftCone J D cc) e =
funExt λ { tt* → cong lift (funExt⁻ (cc .coneOutCommutes e) tt*) }

limSetIso : ∀ J D → CatIso (SET (ℓ-suc ℓ))
(completeSETSuc J (LiftF ∘F D) .lim)
(LiftF .F-ob (completeSET J D .lim))
(completeSETSuc J (LiftF _ ∘F D) .lim)
(LiftF _ .F-ob (completeSET J D .lim))
fst (limSetIso J D) cc = lift (lowerCone J D cc)
cInv (snd (limSetIso J D)) cc = liftCone J D (cc .lower)
sec (snd (limSetIso J D)) = funExt (λ _ → liftExt (cone≡ λ _ → refl))
Expand Down
2 changes: 1 addition & 1 deletion Cubical/Categories/Presheaf/Morphism.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'}
PshHom : Type (ℓ-max (ℓ-max (ℓ-max ℓc ℓc') ℓp) ℓq)
PshHom =
PresheafCategory C (ℓ-max ℓp ℓq)
[ LiftF {ℓp}{ℓq} ∘F P , LiftF {ℓq}{ℓp} ∘F Q ∘F (F ^opF) ]
[ LiftF ℓq ∘F P , LiftF ℓp ∘F Q ∘F (F ^opF) ]

module _ (h : PshHom) where
-- This should define a functor on the category of elements
Expand Down
4 changes: 2 additions & 2 deletions Cubical/Categories/Presheaf/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -394,5 +394,5 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS))

-- Isomorphism between presheaves of different levels
PshIso : (C : Category ℓ ℓ') (P : Presheaf C ℓS) (Q : Presheaf C ℓS') → Type _
PshIso {ℓS = ℓS}{ℓS' = ℓS'} C P Q =
NatIso (LiftF {ℓ = ℓS}{ℓ' = ℓS'} ∘F P) (LiftF {ℓ = ℓS'}{ℓ' = ℓS} ∘F Q)
PshIso {ℓS = ℓS} {ℓS' = ℓS'} C P Q =
NatIso (LiftF ℓS' ∘F P) (LiftF ℓS ∘F Q)
34 changes: 17 additions & 17 deletions Cubical/Categories/Yoneda.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,27 +153,27 @@ module _ {C : Category ℓ ℓ'} where
-- A more universe-polymorphic Yoneda lemma
yoneda* : {C : Category ℓ ℓ'}(F : Functor C (SET ℓ''))
→ (c : Category.ob C)
→ Iso ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-])
, LiftF {ℓ''}{ℓ'} ∘F F ])
→ Iso ((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF ℓ'' ∘F (C [ c ,-])
, LiftF ℓ' ∘F F ])
(fst (F ⟅ c ⟆))
yoneda* {ℓ}{ℓ'}{ℓ''}{C} F c =
((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-])
, LiftF {ℓ''}{ℓ'} ∘F F ])
((FUNCTOR C (SET (ℓ-max ℓ' ℓ''))) [ LiftF ℓ'' ∘F (C [ c ,-])
, LiftF ℓ' ∘F F ])
Iso⟨ the-iso ⟩
((FUNCTOR (LiftHoms C ℓ'')
(SET (ℓ-max ℓ' ℓ''))) [ (LiftHoms C ℓ'' [ c ,-])
, LiftF {ℓ''}{ℓ'} ∘F (F ∘F lowerHoms C ℓ'') ])
Iso⟨ yoneda (LiftF {ℓ''}{ℓ'} ∘F (F ∘F lowerHoms C ℓ'')) c ⟩
Lift {ℓ''}{ℓ'} (fst (F ⟅ c ⟆))
, LiftF ℓ' ∘F (F ∘F lowerHoms C ℓ'') ])
Iso⟨ yoneda (LiftF ℓ' ∘F (F ∘F lowerHoms C ℓ'')) c ⟩
Lift ℓ' (fst (F ⟅ c ⟆))
Iso⟨ invIso LiftIso ⟩
(fst (F ⟅ c ⟆)) ∎Iso where

the-iso : Iso ((FUNCTOR C (SET (ℓ-max ℓ' ℓ'')))
[ LiftF {ℓ'}{ℓ''} ∘F (C [ c ,-])
, LiftF {ℓ''}{ℓ'} ∘F F ])
[ LiftF ℓ'' ∘F (C [ c ,-])
, LiftF ℓ' ∘F F ])
((FUNCTOR (LiftHoms C ℓ'') (SET (ℓ-max ℓ' ℓ'')))
[ (LiftHoms C ℓ'' [ c ,-])
, LiftF {ℓ''}{ℓ'} ∘F (F ∘F lowerHoms C ℓ'') ])
, LiftF ℓ' ∘F (F ∘F lowerHoms C ℓ'') ])
the-iso .fun α .N-ob d f = α .N-ob d f
the-iso .fun α .N-hom g = α .N-hom (g .lower)
the-iso .inv β .N-ob d f = β .N-ob d f
Expand All @@ -184,22 +184,22 @@ yoneda* {ℓ}{ℓ'}{ℓ''}{C} F c =
yonedaᴾ* : {C : Category ℓ ℓ'}(F : Functor (C ^op) (SET ℓ''))
→ (c : Category.ob C)
→ Iso (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ''))
[ LiftF {ℓ'}{ℓ''} ∘F (C [-, c ])
, LiftF {ℓ''}{ℓ'} ∘F F ])
[ LiftF ℓ'' ∘F (C [-, c ])
, LiftF ℓ' ∘F F ])
(fst (F ⟅ c ⟆))
yonedaᴾ* {ℓ}{ℓ'}{ℓ''}{C} F c =
(FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ''))
[ LiftF {ℓ'}{ℓ''} ∘F (C [-, c ]) , LiftF {ℓ''}{ℓ'} ∘F F ]) Iso⟨ the-iso ⟩
[ LiftF ℓ'' ∘F (C [-, c ]) , LiftF ℓ' ∘F F ]) Iso⟨ the-iso ⟩
(FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ''))
[ LiftF {ℓ'}{ℓ''} ∘F ((C ^op) [ c ,-])
, LiftF {ℓ''}{ℓ'} ∘F F ]) Iso⟨ yoneda* F c ⟩
[ LiftF ℓ'' ∘F ((C ^op) [ c ,-])
, LiftF ℓ' ∘F F ]) Iso⟨ yoneda* F c ⟩
fst (F ⟅ c ⟆) ∎Iso where

the-iso :
Iso (FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ''))
[ LiftF {ℓ'}{ℓ''} ∘F (C [-, c ]) , LiftF {ℓ''}{ℓ'} ∘F F ])
[ LiftF ℓ'' ∘F (C [-, c ]) , LiftF ℓ' ∘F F ])
(FUNCTOR (C ^op) (SET (ℓ-max ℓ' ℓ''))
[ LiftF {ℓ'}{ℓ''} ∘F ((C ^op) [ c ,-]) , LiftF {ℓ''}{ℓ'} ∘F F ])
[ LiftF ℓ'' ∘F ((C ^op) [ c ,-]) , LiftF ℓ' ∘F F ])
the-iso .fun α .N-ob = α .N-ob
the-iso .fun α .N-hom = α .N-hom
the-iso .inv β .N-ob = β .N-ob
Expand Down
4 changes: 2 additions & 2 deletions Cubical/Codata/M/Container.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,11 +64,11 @@ shift-chain = λ X,π -> ((λ x → X X,π (suc x)) ,, λ {n} → π X,π {suc n
------------------------------------------------------

Wₙ : ∀ {ℓ} -> Container ℓ -> ℕ -> Type ℓ
Wₙ S 0 = Lift Unit
Wₙ S 0 = Unit*
Wₙ S (suc n) = P₀ S (Wₙ S n)

πₙ : ∀ {ℓ} -> (S : Container ℓ) -> {n : ℕ} -> Wₙ S (suc n) -> Wₙ S n
πₙ {ℓ} S {0} _ = lift tt
πₙ {ℓ} S {0} _ = tt*
πₙ S {suc n} = P₁ (πₙ S {n})

sequence : ∀ {ℓ} -> Container ℓ -> Chain ℓ
Expand Down
4 changes: 2 additions & 2 deletions Cubical/Codata/M/helper.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,9 +81,9 @@ iso→fun-Injection-Iso-x isom {x} {y} =
(λ x₁ → x₁ (lift tt))
(λ x → refl)
(λ x → refl) ⟩
(∀ (t : Lift Unit) -> (((fun isom) ∘ tempx) t ≡ ((fun isom) ∘ tempy) t))
(∀ (t : Unit*) -> (((fun isom) ∘ tempx) t ≡ ((fun isom) ∘ tempy) t))
Iso⟨ iso→Pi-fun-Injection isom ⟩
(∀ (t : Lift Unit) -> tempx t ≡ tempy t)
(∀ (t : Unit*) -> tempx t ≡ tempy t)
Iso⟨ iso (λ x₁ → x₁ (lift tt))
(λ x₁ t → x₁)
(λ x → refl)
Expand Down
Loading