foundations.Cyclic.md.
Version of Sunday, January 22, 2023, 10:42 PM
Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3
{-# OPTIONS --without-K --exact-split #-}
open import foundations.Core using (Level)
module foundations.Cyclic (ℓ : Level)
where
open import foundations.Nat ℓ
open import foundations.Fin ℓ
open import foundations.Core
open import foundations.NaturalsType
cyclic-has-finite-set-properties
: {A : Type ℓ}
→ (A-cyclic : A is-cyclic)
→ (P : Type ℓ → hProp ℓ)
→ ((Fin (n A-cyclic)) has-property P)
→ A has-property P
cyclic-has-finite-set-properties {A = A} A-is-cyclic P Fin-holds-P
= trunc-elim (π₂ (P A)) proof (cyclicity A-is-cyclic)
where
phi : A → A
phi = φ A-is-cyclic
open import foundations.UnivalenceAxiom
abstract
proof
: ∑[ e ∶ (A ≃ Fin (n A-is-cyclic)) ] (phi ︔ (e ∙) ≡ (e ∙) ︔ fin-pred)
→ A has-property P
proof (e , _) = tr (_has-property P) (! (ua e)) (Fin-holds-P)
open import foundations.Finite
is-cyclic-is-finite
: ∀ {A : Type ℓ}
→ A is-cyclic
-------------
→ A is-finite
is-cyclic-is-finite {A = A} A-is-cyclic =
cyclic-has-finite-set-properties A-is-cyclic
(λ X → isFinite X , being-finite-is-prop) Fin-is-finite
is-cyclic-is-set
: ∀ {A : Type ℓ}
→ A is-cyclic
-------------
→ A is-set
is-cyclic-is-set {A = A} A-is-cyclic
= cyclic-has-finite-set-properties A-is-cyclic
(λ t → isSet t , set-is-prop) Fin-is-set
module _ (A : Type ℓ) where
∑s : Type ℓ
∑s = (∑[ φ ∶ (A → A) ]
∑[ n ∶ ℕ ]
∥ ∑ (A ≃ Fin n) (\e → (φ ︔ (e ∙→)) ≡ ((e ∙→) ︔ fin-pred)) ∥)
∑s-≃-CyclicSet : ∑s ≃ CyclicSet A
∑s-≃-CyclicSet = qinv-≃
(λ { (f , n , c) → cyclic-set f n c})
((λ {cset → φ cset , n cset , cyclicity cset})
, (λ {p → idp}) , λ {p → idp})
where open CyclicSet
CyclicSet-≃-∑s : (CyclicSet A) ≃ ∑s
CyclicSet-≃-∑s = ≃-sym ∑s-≃-CyclicSet
module CyclicSet-is-set {A : Type ℓ}
where
module _ (A-is-set : isSet A)
where
abstract
A→A-is-set : isSet (A → A)
A→A-is-set = pi-is-set (λ _ → A-is-set)
∑s-is-set : isSet (∑s A)
∑s-is-set = ∑-set A→A-is-set
(λ f → ∑-set ℕ-is-set (λ _ → prop-is-set truncated-is-prop))
proof' : isSet (CyclicSet A)
proof' = ≃-with-a-set-is-set (∑s-≃-CyclicSet A) ∑s-is-set
abstract
proof : isSet (CyclicSet A)
proof A-is-cyclic = proof' A-is-set A-is-cyclic
where
A-is-set : isSet A
A-is-set = is-cyclic-is-set A-is-cyclic
module _
where
open CyclicSet
cyclic-sets-over-the-same-type-have-same-cardinal
: {A : Type ℓ}
→ (cA cB : CyclicSet A)
→ n cA ≡ n cB
cyclic-sets-over-the-same-type-have-same-cardinal cA cB
= (trunc-elim (ℕ-is-set _ _)
(λ (e₁ , _) -- e₁ : A ≃ Fin (n cA)
→ trunc-elim (ℕ-is-set _ _)
(λ (e₂ , _) -- e₂ : A ≃ Fin (n cB)
→ Fin₁-is-inj-≃ _ _ (≃-trans (≃-sym e₁) e₂))
(cyclicity cB))
(cyclicity cA))
lemma-2-13
: ∀ {A : Type ℓ}
→ (c1 c2 : CyclicSet A)
→ (c1 ≡ c2) ≃ (φ c1 ≡ φ c2)
lemma-2-13 {A = A} c1@(cyclic-set φ1 n1 p1) c2@(cyclic-set φ2 n2 p2) =
begin≃
(c1 ≡ c2)
≃⟨ qinv-≃ (λ { idp → idp}) ((λ { idp → idp} )
, (λ { idp → idp}) , λ {idp → idp}) ⟩
((φ1 , n1) , p1) ≡ ((φ2 , n2) , p2)
≃⟨ simplify-pair (λ _ → trunc-is-prop) ⟩
(φ1 , n1) ≡ (φ2 , n2)
≃⟨ ≃-sym (pair=Equiv _ _) ⟩
(∑[ α ∶ (φ1 ≡ φ2) ] (tr _ α n1 ≡ n2))
≃⟨ fiber-prop-∑-is-base (λ {idp → cyclic-sets-over-the-same-type-have-same-cardinal c1 c2})
(λ {idp → ℕ-is-set _ _}) ⟩
φ1 ≡ φ2
≃∎
lemma-2-14
: (A : Type ℓ) (cA : CyclicSet A)
→ (B : Type ℓ) (cB : CyclicSet B)
→ ((A , cA) ≡ (B , cB))
≃ (∑[ α ∶ A ≡ B ] ((coe α) ∘ φ cA ≡ φ cB ∘ (coe α)))
lemma-2-14 A cA@(cyclic-set φA nA Aprop) B cB@(cyclic-set φB nB Bprop) =
begin≃
((A , cA) ≡ (B , cB))
≃⟨ qinv-≃ (λ { idp → idp}) ((λ { idp → idp} )
, (λ { idp → idp}) , λ {idp → idp}) ⟩
((((A , φA) , nA) , Aprop) ≡ ( (( (B , φB) , nB) , Bprop)))
≃⟨ simplify-pair (λ _ → trunc-is-prop) ⟩
(((A , φA) , nA) ≡ ((B , φB) , nB))
≃⟨ ≃-sym (pair=Equiv _ _) ⟩
(∑[ α ∶ (A , φA) ≡ (B , φB) ] ((tr (λ _ → ℕ) α nA) ≡ nB))
≃⟨ fiber-prop-∑-is-base (λ {idp → cyclic-sets-over-the-same-type-have-same-cardinal cA cB})
(λ {idp → ℕ-is-set _ _}) ⟩
((A , φA) ≡ (B , φB))
≃⟨ ≃-sym (pair=Equiv _ _) ⟩
∑[ α ∶ A ≡ B ] (tr (λ X → X → X) α φA ≡ φB)
≃⟨ sigma-preserves (λ {idp → idEqv}) ⟩
(∑[ α ∶ A ≡ B ] ((coe α) ∘ φ cA ≡ φ cB ∘ (coe α)))
≃∎
charactherization-of-cyclic-sets = lemma-2-14
≡-cardinal-finite-cyclic
: ∀ {A : Type ℓ}
→ ((cyclic-set _ n _) : CyclicSet A)
→ ((m , _) : isFinite A)
→ n ≡ m
≡-cardinal-finite-cyclic (cyclic-set _ n p) (m , q)
= trunc-elim (ℕ-is-set _ _)
(λ {(A≃[n] , _) → trunc-elim (ℕ-is-set _ _) (λ A≃[m] →
Fin₁-is-inj-≃ _ _ (≃-trans (≃-sym A≃[n]) A≃[m])) q}) p
where
open import foundations.Nat
module
_
(∏-finite : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂}
→ isFinite A → ((a : A) → isFinite (B a)) → isFinite (∏ A B))
(∑-finite : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂}
→ isFinite A → ((a : A) → isFinite (B a)) → isFinite (∑ A B)) where
cyclic-set-is-finite
: ∀ {A : Type ℓ}
→ isFinite A
-------------
→ isFinite (CyclicSet A)
cyclic-set-is-finite {A = A} A-is-finite =
equiv-preserves-finiteness (∑s-≃-CyclicSet A)
(∑-finite (∏-finite A-is-finite λ _ → A-is-finite)
λ phi → equiv-preserves-finiteness (≃-sym (helper phi))
(∥∥-finite (∑-finite (≃-finite ∏-finite ∑-finite A-is-finite Fin-is-finite)
λ e → ≡-finite (∏-finite A-is-finite (λ _ → Fin-is-finite)))))
where
m = fst A-is-finite
helper : (phi : A → A)
→ (∑[ n ∶ ℕ ] (∥ ∑[ e ∶ (A ≃ Fin n) ] ((phi ︔ (e ∙→)) ≡ ((e ∙→) ︔ fin-pred)) ∥))
≃ ∥ ∑ (A ≃ Fin m) (λ e → phi ︔ (e ∙→) ≡ (e ∙→) ︔ fin-pred) ∥
helper phi = prop-ext-≃ (λ {(n1 , p1) (n2 , p2)
→ pair= (cyclic-sets-over-the-same-type-have-same-cardinal
(cyclic-set phi n1 p1) (cyclic-set phi n2 p2) , trunc-is-prop _ _)})
trunc-is-prop
((λ{(n , p) →
let helper : n ≡ m
helper = ≡-cardinal-finite-cyclic (cyclic-set phi n p) A-is-finite
in tr _ helper p})
, λ {p → (m , p)})
\begin{proof} It follows from the 2-out-of-3-property that in a commutative triangle if two of the sides are equivalence, the remainder side is also an equivalence. In this case, we have merely the equivalence \(e\) and , and their composition. Since what we want to prove it’s a proposition by propositional truncation elimination the result follows. \begin{minipage}{0.6}
φ-is-equiv
: ∀ {A : Type ℓ}
→ (A-cyclic : CyclicSet A)
→ isEquiv (φ A-cyclic)
\end{minipage}
φ-is-equiv {A = A} C
= trunc-elim (isEquivIsProp phi) proof (cyclicity C)
where
phi : A → A
phi = φ C
abstract
proof
: ∑[ e ∶ A ≃ Fin (n C) ] (phi ︔ (e ∙) ≡ (e ∙) ︔ fin-pred)
→ isEquiv phi
proof (e , p)
= 2-out-of-3-property phi (≃-trans e fin-pred-≃) (≃-sym e) phi-eq
where
phi-eq : phi ≡ (e ∙) ︔ fin-pred ︔ (e ∙←)
phi-eq = move-right-from-composition phi e ((e ∙) ︔ fin-pred) p
Now, we have plain access to the inverse of the function \(φ\) by means of the above equivalence.
φ⁻¹ : ∀ {A : Type ℓ} → CyclicSet A → (A → A)
φ⁻¹ A-cyclic = remap (φ A-cyclic , φ-is-equiv A-cyclic)
\end{proof}
For any \(e : A \simeq B\), and functions \(f : A → A\) and \(g : B → B\) such that $ f ≡ e ; g ; e^{-1}$ then for any \(k : ℕ\), $ f^k ≡ e ; g^{k} ; e^{-1}$.
iterate-k
: ∀ {ℓ₁ ℓ₂ : Level}{A : Type ℓ₁}{B : Type ℓ₂}
→ (e : A ≃ B) → (f : A → A) → (g : B → B)
→ (k : ℕ)
→ f ≡ (e ∙→) ︔ g ︔ (e ∙←)
→ (f ^ k) ≡ (e ∙→) ︔ (g ^ k) ︔ (e ∙←)
iterate-k e f g 0 p = funext (λ a → ! ((rlmap-inverse e) {a}))
where
open import foundations.FunExtAxiom
iterate-k e f g (succ k) p =
begin
f ^ (succ k)
≡⟨ funext (λ a → ap f (happly IH a)) ⟩
((e ∙→) ︔ (g ^ k) ︔ (e ∙←)) ︔ f
≡⟨ ap (_ ︔_ ) p ⟩
((e ∙→) ︔ (g ^ k) ︔ (e ∙←)) ︔ ((e ∙→) ︔ g ︔ (e ∙←))
≡⟨⟩
(e ∙→) ︔ (g ^ k) ︔ ((e ∙←) ︔ (e ∙→)) ︔ (g ︔ (e ∙←))
≡⟨ ap
(λ w → ((((e ∙→) ︔ (g ^ k))) ︔ w ︔ g ︔ (e ∙←)))
(funext (lrmap-inverse-h e)) ⟩
(e ∙→) ︔ (g ^ k) ︔ id ︔ (g ︔ (e ∙←))
≡⟨⟩
(e ∙→) ︔ (g ^ (succ k)) ︔ (e ∙←)
∎
where
open import foundations.FunExtAxiom
IH : (f ^ k) ≡ (e ∙→) ︔ (g ^ k) ︔ (e ∙←)
IH = iterate-k e f g k p
find-k-pred
: ∀ {n : ℕ}
→ (a b : Fin n)
→ ∑ (Fin n) (\k →
((fin-pred ^ (π₁ k)) a ≡ b)
× ((k' : Fin n) → (fin-pred ^ (π₁ k')) a ≡ b → k ≡ k'))
find-k-pred {zero} (zero , ()) (zero , b<n)
find-k-pred {zero} (zero , ()) (succ b , b<n)
find-k-pred {zero} (succ a , ()) (zero , b<n)
find-k-pred {zero} (succ a , ()) (succ b , b<n)
find-k-pred {succ n} (a , a<n+) (b , b<n+)
with trichotomy a b
... | inl (inl a≡b) rewrite a≡b | <-prop {n = succ n}{b} a<n+ b<n+
= ((0 , ∗)) , idp , λ k' p
→ ! (fin-exp-is-unique {n = succ n} k' (zero , ∗) _ p)
... | inl (inr a<b) = ((l +ₙ a) , l+a<n+) , p^l+a≡b
, λ k' p
→ fin-exp-is-unique ((l +ₙ a) , l+a<n+) _ (a , a<n+) (p^l+a≡b · ! p)
where
find-l : ∑ ℕ (\l → (b +ₙ l ≡ succ n) × (0 < l))
find-l = find-x-to-< b<n+
l = proj₁ find-l
l≡ : b +ₙ l ≡ succ n
l≡ = proj₁ (proj₂ find-l)
find-x : ∑ ℕ (\x → (a +ₙ x ≡ b) × (x > 0))
find-x = find-x-to-< a<b
x = proj₁ find-x
x≡ : a +ₙ x ≡ b
x≡ = proj₁ (proj₂ find-x)
p^aa=0 : (fin-pred ^ a) (a , a<n+) ≡ (0 , ∗)
p^aa=0 = p^a-on-a≡0 {n}{a} a<n+
l+a<n+ : (l +ₙ a) < succ n
l+a<n+ = +≡-to-< {l +ₙ a}{succ n} (x , l+a+x≡succn) (proj₂ (proj₂ find-x))
where
l+a+x≡succn : (l +ₙ a) +ₙ x ≡ succ n
l+a+x≡succn =
begin (l +ₙ a) +ₙ x ≡⟨ ! (plus-assoc l a x) ⟩
l +ₙ (a +ₙ x) ≡⟨ plus-comm l (a +ₙ x) ⟩
(a +ₙ x) +ₙ l ≡⟨ ap (_+ₙ l) x≡ ⟩
b +ₙ l ≡⟨ l≡ ⟩
succ n ∎
from-0-to-b : (fin-pred ^ l) (0 , unit) ≡ (b , b<n+)
from-0-to-b = p^l0≡b l≡ b<n+
p^l+a≡b : (fin-pred ^ l +ₙ a) (a , a<n+) ≡ (b , b<n+)
p^l+a≡b =
begin
(fin-pred ^ (l +ₙ a)) (a , a<n+) ≡⟨ i ⟩
(fin-pred ^ l) ((fin-pred ^ a) (a , a<n+)) ≡⟨ ii ⟩
(fin-pred ^ l) (0 , unit) ≡⟨ iii ⟩
(b , b<n+) ∎
where
i = app-comm₂ fin-pred l a _
ii = ap (fin-pred ^ l) p^aa=0
iii = from-0-to-b
... | inr b<a = ((l , l<sucn)) , oo , λ k' p
→ fin-exp-is-unique {n = succ n} (l , l<sucn) k' _ (oo · (! p))
where
find-l : ∑ ℕ (\l → (b +ₙ l ≡ a) × ((0 < l)))
find-l = find-x-to-< b<a
l = proj₁ find-l
l≡ : b +ₙ l ≡ a
l≡ = proj₁ (proj₂ find-l)
sol-2 : ∑ ℕ (\o → ((b +ₙ l) +ₙ o ≡ succ n) × (0 < o))
sol-2 rewrite l≡ = find-x-to-< a<n+
sol = proj₁ sol-2
sol≡ = (proj₂ ︔ proj₁) sol-2
sol>0 = proj₂ (proj₂ sol-2)
b+sol : l +ₙ (b +ₙ sol) ≡ succ n
b+sol = (plus-assoc l b sol) · ap (_+ₙ sol) (plus-comm l b) · sol≡
b+sol>0 : (b +ₙ sol) > 0
b+sol>0 rewrite plus-comm b sol = +>0 {sol}{b} sol>0
l<sucn : l < succ n
l<sucn = +≡-to-< {l}{succ n} ((b +ₙ sol) , b+sol) b+sol>0
oo : (fin-pred ^ l) (a , a<n+) ≡ (b , b<n+)
oo = ! +ₙ-to-fin-pred (b , b<n+) ((a , a<n+)) l l<sucn (l≡)
find-k-succ
: ∀ {n : ℕ}
→ (a b : Fin n)
→ ∑ (Fin n) (\k →
((fin-suc ^ (π₁ k)) a ≡ b)
× ((k' : Fin n) → (fin-suc ^ (π₁ k')) a ≡ b → k ≡ k'))
find-k-succ {n} a b
= k , (! (fin-pred^-to-fin-suc^ b a (π₁ k) k≡))
, λ k' p → unique-k k' (! (fin-suc^-to-fin-pred^ a b ((π₁ k')) p))
where
k-pred
: ∑ (Fin n) (\k → ((fin-pred ^ (π₁ k)) b ≡ a)
× ((k' : Fin n) → (fin-pred ^ (π₁ k')) b ≡ a → k ≡ k'))
k-pred = find-k-pred b a
k = proj₁ k-pred
k≡ = proj₁ (proj₂ k-pred)
unique-k = proj₂ (proj₂ k-pred)
comes-from-cyclicity-is-prop
: ∀ {A : Type ℓ}
→ (A-cyclic : A is-cyclic)
→ (a b : A)
→ isProp (∑ (Fin (n A-cyclic)) (\k →
(((φ A-cyclic) ^ (π₁ k)) a ≡ b)
× ((k' : Fin (n A-cyclic))
→ (((φ A-cyclic) ^ (π₁ k')) a ≡ b)
→ k ≡ k')))
comes-from-cyclicity-is-prop A-cyclic a b ((k , k<) , p , f) ( k' , q , g) =
pair= (f k' q , pair= (is-cyclic-is-set A-cyclic _ _ _ _ ,
pi-is-prop (λ a → pi-is-prop (λ b → Fin-is-set k' a)) _ _))
ccw-steps-in_from_to_
: ∀ {A : Type ℓ}
→ (A↺ : A is-cyclic)
→ (a b : A)
→ ∑[ k ∶ Fin (n A↺) ] (((φ A↺) ^ (π₁ k)) a ≡ b)
× (∏[ k' ∶ Fin (n A↺)] ((((φ A↺) ^ (π₁ k')) a ≡ b) → k ≡ k'))
ccw-steps-in A-cyclic from a to b
= trunc-elim (comes-from-cyclicity-is-prop A-cyclic a b) proof (cyclicity A-cyclic)
where
phi = φ A-cyclic
A = domain (φ A-cyclic)
proof
: ∑ (domain phi ≃ Fin (n A-cyclic)) (λ e → phi ︔ (e ∙) ≡ (e ∙) ︔ fin-pred)
→ ∑ (Fin (n A-cyclic)) (\k → (((φ A-cyclic) ^ (π₁ k)) a ≡ b)
× ((k' : Fin (n A-cyclic)) → (((φ A-cyclic) ^ (π₁ k')) a ≡ b) → k ≡ k'))
proof (e , p) =
finK , ((begin
(phi ^ k) a
≡⟨ happly (iterate-k e phi fin-pred k phi-eq) a ⟩
(e ∙←) ((fin-pred ^ k) ((e ∙→) a))
≡⟨ ap (e ∙←) (proj₁ (proj₂ k*)) ⟩
(e ∙←) ((e ∙→) b)
≡⟨ rlmap-inverse e ⟩
b ∎) , λ k' q → proj₂ (proj₂ k*) k'
(begin
(fin-pred ^ proj₁ k') ((e ∙→) a)
≡⟨ (happly (! (fun-power {k = proj₁ k'})) a) ⟩
(e ∙→) ((phi ^ proj₁ k') a)
≡⟨ ap (e ∙→) q ⟩
(e ∙→) b
∎))
where
open import foundations.FunExtAxiom
phi-eq : phi ≡ (e ∙) ︔ fin-pred ︔ (e ∙←)
phi-eq = move-right-from-composition phi e ((e ∙) ︔ fin-pred) p
fun-power : ∀ {k} → (phi ^ k) ︔ (e ∙→) ≡ (e ∙→) ︔ (fin-pred ^ k)
fun-power {k} =
move-left-from-composition (phi ^ k) e ((e ∙→) ︔ (fin-pred ^ k) )
(iterate-k e phi fin-pred k phi-eq)
k* : ∑ (Fin (n A-cyclic)) (\k
→ ((fin-pred ^ proj₁ k) ((e ∙→) a) ≡ (e ∙→) b)
× ((k' : Fin (n A-cyclic))
→ ((fin-pred ^ proj₁ k') ((e ∙→) a) ≡ (e ∙→) b)
→ k ≡ k'))
k* = find-k-pred _ _
finK = proj₁ k*
k = proj₁ (proj₁ k*)
φ-cyclic-has-finite-set-properties
: {A : Type ℓ}
→ (A-cyclic : A is-cyclic)
→ (P : ∀ {X}{Y} → (X → Y) → hProp ℓ)
→ (fin-pred {k = n A-cyclic}) has-fun-property P
→ (φ A-cyclic) has-fun-property P
φ-cyclic-has-finite-set-properties {A = A} A-cyclic P Fin-holds-P
= trunc-elim (π₂ (P (φ A-cyclic))) proof (cyclicity A-cyclic)
where
phi = φ A-cyclic
proof
: ∑ (A ≃ Fin (n A-cyclic)) (λ e → phi ︔ (e ∙) ≡ (e ∙) ︔ fin-pred)
→ φ A-cyclic has-fun-property P
proof (e , p) = tr₂ (λ X f → f has-fun-property P) e-bar tr-pred-phi Fin-holds-P
where
phi-eq : phi ≡ (e ∙) ︔ fin-pred ︔ (e ∙←)
phi-eq = move-right-from-composition phi e ((e ∙) ︔ fin-pred) p
open import foundations.UnivalenceAxiom
open import foundations.UnivalenceLemmas
open import foundations.UnivalenceTransport
open import foundations.FunExtAxiom
e-bar : Fin (n A-cyclic) ≡ A
e-bar = ua (≃-sym e)
minilemma : ! e-bar ≡ ua e
minilemma = ap !_ (ua-inv e) · involution (ua e)
tr-pred-phi : (tr (λ X → (X → X)) e-bar fin-pred) ≡ phi
tr-pred-phi =
begin
tr (λ X → (X → X)) e-bar fin-pred
≡⟨ transport-fun e-bar fin-pred ⟩
(λ a → tr (λ z → z) e-bar (fin-pred (tr (λ z → z) (! e-bar) a)))
≡⟨ funext (λ a → coe-ua (≃-sym e)
(fin-pred (tr (λ z → z) (! e-bar) a)) ) ⟩
(λ a → (e ∙←) (fin-pred (tr (λ z → z) (! e-bar) a)))
≡⟨ funext (λ a → ap (fin-pred ︔ (e ∙←))
(ap (λ w → tr (λ z → z) w a) minilemma)) ⟩
(λ a → (e ∙←) (fin-pred (tr (λ z → z) (ua e) a)))
≡⟨ funext (λ a → ap (fin-pred ︔ (e ∙←)) (coe-ua e a)) ⟩
(λ a → (e ∙←) (fin-pred ((e ∙→) a)))
≡⟨ funext (λ a → happly (! phi-eq) a) ⟩
phi
∎
φ⁻¹-cyclic-has-finite-set-properties
: {A : Type ℓ}
→ (A-cyclic : A is-cyclic)
→ ∀ {ℓ₂ : Level} → (P : ∀ {X : Type ℓ} → (X → X) → hProp ℓ₂)
→ (fin-suc {n = n A-cyclic}) has-endo-property P
→ (φ⁻¹ A-cyclic) has-endo-property P
φ⁻¹-cyclic-has-finite-set-properties {A = A} A-cyclic P Fin-holds-P
= trunc-elim (π₂ (P (φ⁻¹ A-cyclic))) proof (cyclicity A-cyclic)
where
phi = φ A-cyclic
invphi = φ⁻¹ A-cyclic
proof
: ∑ (A ≃ Fin (n A-cyclic)) (λ e → phi ︔ (e ∙) ≡ (e ∙) ︔ fin-pred)
→ (φ⁻¹ A-cyclic) has-endo-property P
proof (e , p) = tr₂ (λ X f → f has-endo-property P) e-bar tr-suc-invphi Fin-holds-P
where
phi-eq : phi ≡ (e ∙) ︔ fin-pred ︔ (e ∙←)
phi-eq = move-right-from-composition phi e ((e ∙) ︔ fin-pred) p
e-equiv : A ≃ Fin (n A-cyclic)
e-equiv = e
inv-phi-eq : invphi ≡ ((e ∙→) ︔ fin-suc) ︔ (e ∙←)
inv-phi-eq =
begin
invphi
≡⟨⟩
remap (φ A-cyclic , φ-is-equiv A-cyclic)
≡⟨ ap {A = A ≃ A}{A → A} (remap {A = A}{B = A}) {(φ A-cyclic , φ-is-equiv A-cyclic)}{(≃-trans (≃-trans e fin-pred-≃) (≃-sym e))} (sameEqv phi-eq) ⟩
remap (≃-trans (≃-trans e fin-pred-≃) (≃-sym e))
≡⟨ inv-of-equiv-composition {A = A}{B = Fin _}{C = A} (≃-trans e fin-pred-≃) (≃-sym e) ⟩
(e ∙→) ︔ (remap (≃-trans e fin-pred-≃))
≡⟨ ap ((e ∙→) ︔_) (inv-of-equiv-composition e fin-pred-≃) ⟩
(e ∙→) ︔ ((fin-pred-≃ ∙←) ︔ (e ∙←))
≡⟨ idp ⟩
((e ∙→) ︔ fin-suc) ︔ (e ∙←)
∎
open import foundations.UnivalenceAxiom
open import foundations.UnivalenceLemmas
open import foundations.UnivalenceTransport
open import foundations.FunExtAxiom
e-bar : Fin (n A-cyclic) ≡ A
e-bar = ua (≃-sym e)
minilemma : ! e-bar ≡ ua e
minilemma = ap !_ (ua-inv e) · involution (ua e)
tr-suc-invphi : (tr (λ X → (X → X)) e-bar fin-suc) ≡ invphi
tr-suc-invphi =
begin
tr (λ X → (X → X)) e-bar fin-suc
≡⟨ transport-fun e-bar fin-suc ⟩
(λ a → tr (λ z → z) e-bar (fin-suc (tr (λ z → z) (! e-bar) a)))
≡⟨ funext (λ a → coe-ua (≃-sym e) (fin-suc (tr (λ z → z) (! e-bar) a)) ) ⟩
(λ a → (e ∙←) (fin-suc (tr (λ z → z) (! e-bar) a)))
≡⟨ funext (λ a → ap (fin-suc ︔ (e ∙←))
(ap (λ w → tr (λ z → z) w a) minilemma)) ⟩
(λ a → (e ∙←) (fin-suc (tr (λ z → z) (ua e) a)))
≡⟨ funext (λ a → ap (fin-suc ︔ (e ∙←)) (coe-ua e a)) ⟩
(λ a → (e ∙←) (fin-suc ((e ∙→) a)))
≡⟨ funext (λ a → happly (! inv-phi-eq) a) ⟩
invphi
∎ where open import foundations.FunExtAxiom
cw-steps-in_from_to_
: ∀ {A : Type ℓ}
→ (A↺ : A is-cyclic)
→ (a b : A)
→ ∑ (Fin (n A↺ )) (\k → (((φ⁻¹ A↺) ^ (π₁ k)) a ≡ b)
× ((k' : Fin (n A↺ )) → ((φ⁻¹ A↺) ^ (π₁ k')) a ≡ b → k ≡ k'))
cw-steps-in A-cyclic from a to b
= (φ⁻¹-cyclic-has-finite-set-properties
A-cyclic
(λ {X} f → ((_ : isSet X) → (a b : X)
→ ∑ (Fin (n (A-cyclic))) (\k → ((f ^ (π₁ k)) a ≡ b) × ( ∀ k'
→ ((f ^ (π₁ k')) a ≡ b) → k ≡ k'))) ,
-- the above thing it's a proposition.
( (pi-is-prop (λ X-is-set
→ pi-is-prop (λ aa → pi-is-prop (λ bb
→ λ {((k , k<) , p , f) ( k' , q , g)
→ pair= (f k' q , pair= (X-is-set _ _ _ _ ,
pi-is-prop (λ a → pi-is-prop (λ b → Fin-is-set k' a)) _ _))}
))))))
λ X-is-set → find-k-succ ) (is-cyclic-is-set A-cyclic) a b
(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides (2022-07-06)(d3a4a8cf) minors by jonathan.cubides (2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides (2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides (2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides (2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides (2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides (2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides (2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides (2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides (2021-12-15)(0630ce66) Minor fixes by jonathan.cubides (2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides (2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides (2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides (2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides