foundations.Fin.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.Fin (ℓ : Level)
where
open import foundations.Nat ℓ
open import foundations.Core
open import foundations.NaturalsType
open import foundations.TypesofMorphisms
open import foundations.TruncationType
Fin : ℕ → Type ℓ
Fin n = Σ[ m ∶ ℕ ] (m < n)
syntax Fin n = ⟦ n ⟧
bound-of : ∀ {n : ℕ} → Fin n → ℕ
bound-of {n = n} _ = n
𝟘-≃-⟦0⟧ : 𝟘 ℓ ≃ Fin 0
𝟘-≃-⟦0⟧ = qinv-≃ (λ {()}) ((λ { (zero , ())
; (succ _ , ())}) , (λ { (zero , ())
; (succ _ , ())}) , λ { ()})
𝟙-≃-⟦1⟧ : 𝟙 ℓ ≃ Fin 1
𝟙-≃-⟦1⟧ = qinv-≃ (λ { ∗ → zero , ∗}) ((λ _ → ∗) ,
(λ { (zero , ∗) → idp ; (succ n , p) → ⊥-elim (n<0 {ℓ} {n} p)}) , λ { ∗ → idp})
π₁-fin
: ∀ {k : ℕ} {fm1 fm2 : ⟦ k ⟧ }
→ fm1 ≡ fm2
→ π₁ {A = ℕ}{B = λ a → a < k} fm1 ≡ π₁ fm2
π₁-fin = ap π₁
open dec-<
_fin<_ : ∀ {n : ℕ} → ⟦ n ⟧ → ⟦ n ⟧ → Type ℓ
(n , _) fin< (m , _)
with n ?< m
... | yes _ = ⊤ ℓ
... | no _ = ⊥ ℓ
_?fin<_ : ∀ {n : ℕ} → Decidable {A = ⟦ n ⟧} (_fin<_ {n})
(n , _) ?fin< (m , _)
with n ?< m
... | yes p = yes ∗
... | no ¬p = no λ z → z
fin-pred : ∀ {k : ℕ} → ⟦ k ⟧ → ⟦ k ⟧
fin-pred {zero} (zero , ())
fin-pred {succ n} (zero , ★) = n , <-succ n
fin-pred {succ k} (succ m , p) = m , n⁺<k→n<k {m}{succ k} p
fin-pred-inj
: ∀ {k : ℕ} → {x y : ⟦ k ⟧}
→ fin-pred x ≡ fin-pred y
-------------------------
→ x ≡ y
fin-pred-inj {k} {n , n<} {m , m<} p with n ≟nat m
fin-pred-inj {k} {n , n<} {.n , m<} p | yes idp rewrite <-prop {k}{n} n< m< = idp
fin-pred-inj {zero} {zero , ()} {zero , m<} p | no ¬p
fin-pred-inj {zero} {zero , n<} {succ m , ()} p | no ¬p
fin-pred-inj {zero} {succ n , ()} {zero , m<} p | no ¬p
fin-pred-inj {zero} {succ n , n<} {succ m , ()} p | no ¬p
fin-pred-inj {succ k} {zero , ★} {zero , ★} p | no ¬p = idp
fin-pred-inj {succ k} {zero , ★} {succ m , m<} p | no ¬p
= ⊥-elim (<-=-→⊥ m< (! (π₁ (Σ-componentwise p))))
fin-pred-inj {succ k} {succ n , n<} {zero , ★} p | no ¬p
= ⊥-elim (<-=-→⊥ n< (π₁ (Σ-componentwise p)))
fin-pred-inj {succ k} {succ n , n<} {succ m , m<} p | no ¬p
= ⊥-elim (¬p (ap succ (π₁ (Σ-componentwise p))))
pp
: ∀ {k : ℕ} {x : Fin (succ (succ (succ k)))}
→ ((fin-pred (fin-pred x)) ≡ x) → ⊥ ℓ
pp {zero} {zero , π₄} ()
pp {zero} {succ zero , ★} ()
pp {zero} {succ (succ zero) , ★} ()
pp {zero} {succ (succ (succ m)) , π₄} p = n<0 {n = m} π₄
pp {succ k} {zero , ★} ()
pp {succ k} {succ zero , ★} ()
pp {succ k} {succ (succ zero) , ★} ()
pp {succ k} {succ (succ (succ m)) , m<s} p = kkk (π₁-fin p)
where
kkk : ∀ {m : ℕ} → (succ m ≡ succ (succ (succ m))) → ⊥ ℓ
kkk {zero} ()
kkk {succ m} ()
bot1 ⊥-from-fin-predx=y+x=fin-predy
: {k : ℕ} → {x y : Fin (succ (succ (succ k)))}
→ (fin-pred x ≡ y)
→ (x ≡ fin-pred y)
→ ⊥ ℓ
bot1 {k} {x} {y} p q = pp {x = x} ((ap fin-pred p) · ! q)
⊥-from-fin-predx=y+x=fin-predy = bot1
module FinDecidable {n : ℕ} where
_≟fin_ : Decidable {A = ⟦ n ⟧} _≡_
(zero , a<n) ≟fin (zero , b<n) rewrite <-prop {n}{zero} a<n b<n = yes (pair= (idp , idp))
(zero , a<n) ≟fin (succ b , b<n) = no (λ ())
(succ a , a<n) ≟fin (zero , b<n) = no (λ ())
(succ a , a<n) ≟fin (succ b , b<n) with a ≟nat b
... | yes idp rewrite <-prop {n}{succ a} a<n b<n = yes (pair= (idp , idp))
... | no ¬p = no (λ r → ⊥-elim (¬p (nat-succ-inj (π₁ (Σ-componentwise r)))))
open FinDecidable public
FinIsDec
: ∀ {k : ℕ}
→ (n m : ⟦ k ⟧)
→ (n ≡ m) + ((n ≡ m) → ⊥ ℓ)
FinIsDec {k} (n , p1) (m , p2) with n ≟nat m
... | yes idp rewrite <-prop {n = k}{m = n} p1 p2
= inl (pair= (idp , idp))
... | no ¬p = inr (λ par → ⊥-elim (¬p (ap π₁ par)))
Fin-is-decidable = FinIsDec
FinIsSet : ∀ {n : ℕ} → isSet (⟦ n ⟧)
FinIsSet = hedberg FinIsDec
Fin-is-set = FinIsSet
We can show FinisDec is a proposition. In doing so, we only need to take care of the final coproduct because of the nested pi-types. Now, being a propostion for a coproduct implies we must prove that we can find inhabitants for each type but not for both, that’s the goal below.
FinIsDec-is-prop
: ∀ {k : ℕ} → isProp ((n m : Fin k) → (n ≡ m) + (n ≡ m → ⊥ ℓ))
FinIsDec-is-prop = pi-is-prop (λ a →
pi-is-prop (λ b → +-prop (Fin-is-set _ _)
(pi-is-prop (λ p → ⊥-is-prop))
λ { (a≡b , ¬a≡b) → ¬a≡b a≡b}))
where
open HLevelLemmas
_≠Fin_ : ∀ {k : ℕ} (n m : ⟦ k ⟧) → Type ℓ
n ≠Fin m = (n ≡ m) → ⊥ ℓ
fin-pred-sur
: ∀ {k : ℕ}
→ (y : ⟦ k ⟧)
→ Σ[ x ∶ ⟦ k ⟧ ] (fin-pred x ≡ y)
fin-pred-sur {zero} (0 , ())
fin-pred-sur {zero} (succ n , ())
fin-pred-sur {succ k} (n , p) with k ≟nat n
fin-pred-sur {succ k} (.k , p) | yes idp rewrite <-prop {succ k}{k} p (<-succ k) = (zero , ★) , idp
fin-pred-sur {succ k} (0 , unit) | no ¬p = (1 , k≠0-k>0 ¬p) , idp
fin-pred-sur {succ k} (succ n , p) | no ¬p rewrite <-prop {succ k}{succ n} p (n⁺<k→n<k {n}{k} (<-suc-suc< p ¬p)) = (succ (succ n) , <-suc-suc< p ¬p) , idp
fin-pred-IsSurjection
: ∀ {n : ℕ} → isSurjection (fin-pred {n})
fin-pred-IsSurjection b = ∣ (fin-pred-sur b) ∣
fin-pred-equiv fin-pred-≃ : ∀ {n : ℕ} → ⟦ n ⟧ ≃ ⟦ n ⟧
fin-pred-equiv {n}
= Bijection (FinIsSet {n}) (FinIsSet {n}) fin-pred (fin-pred-inj , fin-pred-IsSurjection)
fin-pred-≃ = fin-pred-equiv
fin-pred⁻¹ fin-suc : {n : ℕ} → ⟦ n ⟧ → ⟦ n ⟧
fin-pred⁻¹ = remap fin-pred-equiv
fin-suc = fin-pred⁻¹
fin-pred∘inverse-of-fin-pred
: ∀ {n : ℕ}
→ (x : ⟦ n ⟧)
→ fin-pred (fin-pred⁻¹ x) ≡ x
fin-pred∘inverse-of-fin-pred {n} x = (∙→∘∙← fin-pred-equiv) {b = x}
inverse-of-fin-pred∘fin-pred
: {n : ℕ}
→ (x : ⟦ n ⟧)
→ (fin-pred⁻¹ (fin-pred x)) ≡ x
inverse-of-fin-pred∘fin-pred {n} x = (∙←∘∙→ fin-pred-equiv) {a = x}
fin-pred-is-fin-pred
: (n : ℕ)
→ (fin-pred-equiv {n = succ (succ (succ n))} ∙) ≡ fin-pred
fin-pred-is-fin-pred n = idp
fin-suc︔fin-pred∼id
: ∀ {n : ℕ} → (fin-pred {n} ∘ fin-suc {n}) ∼ id
fin-suc︔fin-pred∼id {n} = lrmap-inverse-h (fin-pred-≃ {n})
fin-pred︔fin-suc∼id
: ∀ {k : ℕ} → (fin-suc {k} ∘ fin-pred {k}) ∼ id
fin-pred︔fin-suc∼id {k} = rlmap-inverse-h (fin-pred-≃ {k})
fin-suc-is-equiv : ∀ {n : ℕ} → ⟦ n ⟧ ≃ ⟦ n ⟧
fin-suc-is-equiv
= qinv-≃ fin-suc
(fin-pred , (λ _ → inverse-of-fin-pred∘fin-pred _)
, λ _ → fin-pred∘inverse-of-fin-pred _)
fin-suc-inj
: ∀ {k : ℕ} → {x y : ⟦ k ⟧}
→ fin-suc x ≡ fin-suc y
-------------------------
→ x ≡ y
fin-suc-inj {x = x}{y} p
= ! (lrmap-inverse-h fin-pred-equiv x) · q · lrmap-inverse-h fin-pred-equiv y
where
q : fin-pred (fin-suc x) ≡ fin-pred (fin-suc y)
q = ap fin-pred p
abstract
fin-suc^-to-fin-pred^
: ∀ {n : ℕ}
→ (k k' : ⟦ n ⟧)
→ (x : ℕ)
→ (fin-suc {n} ^ x) k ≡ k'
→ k ≡ (fin-pred ^ x) k'
fin-suc^-to-fin-pred^ k k' 0 p = p
fin-suc^-to-fin-pred^ k k' (succ x) p = IH · ! app-comm fin-pred x _
where
IH : k ≡ (fin-pred ^ x) (fin-pred k')
IH = fin-suc^-to-fin-pred^ k (fin-pred k') x
((! fin-pred∘inverse-of-fin-pred _ ) · ap fin-pred p)
abstract
fin-pred^-to-fin-suc^
: ∀ {n : ℕ}
→ (k k' : ⟦ n ⟧)
→ (x : ℕ)
→ (fin-pred {n} ^ x) k ≡ k'
→ k ≡ (fin-suc ^ x) k'
fin-pred^-to-fin-suc^ {n} k k' 0 p = p
fin-pred^-to-fin-suc^ {n} k k' (succ x) p = IH · ! app-comm fin-suc x _
where
IH : k ≡ (fin-suc ^ x) (fin-suc k')
IH = fin-pred^-to-fin-suc^ k (fin-suc k') x
((! inverse-of-fin-pred∘fin-pred _ ) · ap fin-suc p)
abstract
+ₙ-to-fin-suc
: ∀ {n : ℕ}
→ (k k' : ⟦ n ⟧)
→ (e : ℕ) → (e < n)
→ (π₁ k) +ₙ e ≡ (π₁ k')
→ (fin-suc ^ e) k ≡ k'
+ₙ-to-fin-suc {succ n} (zero , ∗) (zero , ∗) zero = λ _ _ → idp
+ₙ-to-fin-suc {succ n} (zero , ∗) (succ k' , p') zero p ()
+ₙ-to-fin-suc {succ n} (succ k , p) (zero , ∗) zero = λ _ ()
+ₙ-to-fin-suc {succ n} (succ k , p) (succ .(plus k 0) , p') zero ∗ idp
rewrite plus-runit k = pair= (idp , <-prop {n = n}{m = k} p p') --FIXME: replace this rewrite
+ₙ-to-fin-suc {succ n} (zero , ∗) (zero , ∗) (succ pa) = λ _ ()
+ₙ-to-fin-suc {succ n} (succ k , p) (zero , ∗) (succ pa) q ()
+ₙ-to-fin-suc {n@(succ _)} k@(zero , ∗) (succ k' , p) (succ x) x<n q
--FIXME: this is totally a copy of the next proof-step, it's really awful.
= fin-pred-inj
$ begin
fin-pred (fin-suc ((fin-suc ^ x) k))
≡⟨ fin-suc︔fin-pred∼id _ ⟩
(fin-suc {n} ^ x) k
≡⟨ +ₙ-to-fin-suc k (k' , o) x o' p1 ⟩
(k' , n⁺<k→n<k {k'}{n} p )
≡⟨ p2 ⟩
fin-pred (succ k' , p)
∎
where
-- n = bound-of k
o : k' < n
o = n⁺<k→n<k {k'}{n} p
o' : x < n
o' = (n⁺<k→n<k {x} {n} x<n)
p1 : (π₁ k) +ₙ x ≡ k'
p1 = succ-inj q
where open import foundations.NaturalsType
p2
: ∀ {k' n : ℕ}{p}
→ (k' , n⁺<k→n<k {k'}{n} p) ≡ fin-pred {n} (succ k' , p)
p2 {zero} {succ n} {p} = idp
p2 {succ k'} {succ n} {p} = idp
+ₙ-to-fin-suc {n@(succ _)} k@(succ _ , _) K'@(succ k' , p) (succ x) x<n q
= fin-pred-inj
$ begin
fin-pred (fin-suc ((fin-suc ^ x) k))
≡⟨ fin-suc︔fin-pred∼id _ ⟩
(fin-suc {n} ^ x) k
≡⟨ +ₙ-to-fin-suc k (k' , o) x o' p1 ⟩
(k' , n⁺<k→n<k {k'}{n} p )
≡⟨ p2 ⟩
fin-pred (succ k' , p)
∎
where
-- n = bound-of k
o : k' < n
o = n⁺<k→n<k {k'}{n} p
o' : x < n
o' = (n⁺<k→n<k {x} {n} x<n)
p1 : (π₁ k) +ₙ x ≡ k'
p1 rewrite ! plus-succ (π₁ k) x = succ-inj q
where open import foundations.NaturalsType
p2
: ∀ {k' n : ℕ}{p}
→ (k' , n⁺<k→n<k {k'}{n} p) ≡ fin-pred {n} (succ k' , p)
p2 {zero} {succ n} {p} = idp
p2 {succ k'} {succ n} {p} = idp
abstract
+ₙ-to-fin-pred
: ∀ {n : ℕ}
→ (k k' : ⟦ n ⟧)
→ (x : ℕ) → (x < n)
→ (π₁ k) +ₙ x ≡ (π₁ k')
→ k ≡ (fin-pred {n} ^ x) k'
+ₙ-to-fin-pred k k' x x<n p
= fin-suc^-to-fin-pred^ k k' x (+ₙ-to-fin-suc k k' x x<n p)
abstract
succ-pred-comm' : ∀ {n l : ℕ} → ∀ x
→ (fin-pred {n}) ((fin-suc ^ (succ l)) x)
≡ (fin-suc ^ (succ l)) (fin-pred x)
succ-pred-comm' {l = l} x =
begin
(fin-pred) ((fin-suc ^ (succ l)) x)
≡⟨ fin-suc︔fin-pred∼id _ ⟩
(fin-suc ^ l) x
≡⟨ ap ((fin-suc) ^ l) (! (fin-pred︔fin-suc∼id x)) ⟩
(fin-suc ^ l) (fin-suc (fin-pred x))
≡⟨ ! (app-comm fin-suc l _) ⟩
(fin-suc ^ (succ l)) (fin-pred x)
∎
abstract
succ-pred-comm''
: ∀ {n m : ℕ} → ∀ x
→ (fin-suc {n}) ((fin-pred ^ m) x)
≡ (fin-pred ^ m) (fin-suc x)
succ-pred-comm'' {m = zero} x = idp
succ-pred-comm'' {m = succ l} x =
begin
(fin-suc) ((fin-pred ^ (succ l)) x)
≡⟨ fin-pred︔fin-suc∼id _ ⟩
(fin-pred ^ l) x
≡⟨ ap ((fin-pred) ^ l) (! (fin-suc︔fin-pred∼id x)) ⟩
(fin-pred ^ l) (fin-pred (fin-suc x))
≡⟨ ! (app-comm fin-pred l _) ⟩
(fin-pred ^ (succ l)) (fin-suc x)
∎
abstract
succ-pred-comm
: ∀ {n : ℕ}{k l : ℕ}
→ k < n → l < n
→ ∀ x
→ (fin-pred {n} ^ k) ((fin-suc ^ l) x)
≡ (fin-suc ^ l) ((fin-pred ^ k) x)
succ-pred-comm {succ n} {zero} {zero} k<n l<n x = idp
succ-pred-comm {succ n} {zero} {succ l} k<n l<n x = idp
succ-pred-comm {succ n} {succ k} {zero} k<n l<n x = idp
succ-pred-comm {succ n} {succ k} {succ l} k<n l<n x =
begin
(fin-pred ^ (succ k)) ((fin-suc ^ (succ l)) x)
≡⟨ ap fin-pred IH₁ ⟩
(fin-pred $ (fin-suc ^ (succ l)) ((fin-pred ^ k) x))
≡⟨ succ-pred-comm' {n = succ n }{l = l} _ ⟩
(fin-suc ^ succ l) (fin-pred ((fin-pred ^ k) x))
≡⟨⟩
(fin-suc ^ (succ l)) ((fin-pred ^ (succ k)) x)
∎
where
IH₁ : (fin-pred {succ n} ^ k) ((fin-suc ^ (succ l)) x)
≡ (fin-suc ^ (succ l)) ((fin-pred ^ k) x)
IH₁ = succ-pred-comm {succ n}{k}{succ l} (n⁺<k→n<k {k}{succ n} k<n)
(l<n) x
abstract
unique-exp-fin-pred
: ∀ {n : ℕ}
→ (k : ℕ) → (k < n)
→ (k' : ℕ) → (k' < n)
→ (fin-pred ^ k) ≡ (fin-pred {n} ^ k')
--------------------------------------
→ k ≡ k'
unique-exp-fin-pred 0 _ 0 _ _ = idp
unique-exp-fin-pred {0} 0 _ (succ k') k'< _ = ⊥-elim (n<0 {ℓ}{n = succ k'} k'<)
unique-exp-fin-pred {(succ n)} 0 q (succ k') k'< p = ap proj₁
(begin
(0 , q)
≡⟨ ! happly o (0 , q) ⟩
(fin-suc ^ (succ k')) (0 , q)
≡⟨ +ₙ-to-fin-suc {(succ n)} _ _ (succ k') k'< idp ⟩
(succ k' , k'<)
∎)
where
open import foundations.FunExtAxiom
o : fin-suc {succ n} ^ (succ k') ≡ id
o = funext (λ z → ! fin-pred^-to-fin-suc^ z z (succ k') (happly (! p) z))
-- -- The following is symmetric case of the aboe.
unique-exp-fin-pred {succ n} (succ k) k+< 0 p q
= ! ap proj₁
(begin
(0 , p)
≡⟨ ! happly o (0 , p) ⟩
(fin-suc ^ (succ k)) (0 , p)
≡⟨ +ₙ-to-fin-suc _ _ (succ k) k+< idp ⟩
(succ k , k+<)
∎)
where
open import foundations.FunExtAxiom
o : fin-suc {succ n} ^ (succ k) ≡ id
o = funext (λ z → ! fin-pred^-to-fin-suc^ z z (succ k) (happly q z))
unique-exp-fin-pred {succ n} (succ k) k+< (succ k') k'+< p
= ap succ IH
where
n' : ℕ
n' = bound {k = succ k} k+<
open import foundations.FunExtAxiom
IH : k ≡ k'
IH = unique-exp-fin-pred k
(n⁺<k→n<k {n = k}{k = n'} k+<) k'
(n⁺<k→n<k {n = k'}{k = n'} k'+<)
(funext (λ a → fin-pred-inj $ happly p a))
abstract
change-point-fin-pred'
: ∀ {n k : ℕ}
→ k < n
→ (fin-pred {n} ^ k) ≡ id
→ k ≡ 0
change-point-fin-pred' {zero} {k} k< p = ⊥-elim (n<0 {ℓ} {n = k} k<)
change-point-fin-pred' {succ n} {k} k< p = unique-exp-fin-pred k k< 0 ∗ p
change-point-fin-pred
: ∀ {n k : ℕ} {x : ⟦ n ⟧}
→ k < n
→ (fin-pred ^ k) x ≡ x
→ k ≡ 0
change-point-fin-pred {succ n} {zero} ∗ p = idp
change-point-fin-pred {succ n} {k@(succ _)} {(x , x<n)} k<n p
= change-point-fin-pred' k<n (funext o)
where
open import foundations.FunExtAxiom
o : ∀ y → (fin-pred {succ n} ^ k) y ≡ y
o (y , y<)
with trichotomy x y
... | inl (inl x≡y) rewrite ! x≡y | <-prop {succ n}{x} y< x<n = p
... | inl (inr x<y) =
begin
(fin-pred ^ k) (y , y<)
≡⟨ ap (fin-pred ^ k) (! s^lx≡y) ⟩
(fin-pred ^ k) ((fin-suc ^ l) (x , x<n))
≡⟨ succ-pred-comm {n = succ n}{k = k}{l = l} k<n l<sucn (x , x<n) ⟩
(fin-suc ^ l) ((fin-pred ^ k) (x , x<n))
≡⟨ ap (fin-suc ^ l) p ⟩
(fin-suc ^ l) (x , x<n)
≡⟨ s^lx≡y ⟩
(y , y<)
∎
where
find-l : ∑ ℕ (\l → (x +ₙ l ≡ y) × (0 < l))
find-l = find-x-to-< x<y
l : ℕ
l = proj₁ find-l
l≡ : x +ₙ l ≡ y
l≡ = proj₁ (proj₂ find-l)
sol-2 : ∑ ℕ (\o → ((x +ₙ l) +ₙ o ≡ succ n) × (0 < o))
sol-2 rewrite l≡ = find-x-to-< y<
sol : ℕ
sol = proj₁ sol-2
sol≡ : (x +ₙ l) +ₙ sol ≡ (succ n)
sol≡ = (proj₂ ︔ proj₁) sol-2
sol>0 : 0 < sol
sol>0 = proj₂ (proj₂ sol-2)
x+sol : l +ₙ (x +ₙ sol) ≡ succ n
x+sol = (plus-assoc l x sol) · ap (_+ₙ sol) (plus-comm l x) · sol≡
x+sol>0 : (x +ₙ sol) > 0
x+sol>0 rewrite plus-comm x sol = +>0 {sol}{x} sol>0
l<sucn : l < succ n
l<sucn = +≡-to-< {l}{succ n} ((x +ₙ sol) , x+sol) x+sol>0
s^lx≡y : (fin-suc ^ l) ((x , x<n)) ≡ (y , y<)
s^lx≡y = (+ₙ-to-fin-suc (x , x<n) (y , y<) l l<sucn l≡)
... | inr y<x =
begin
(fin-pred ^ k) (y , y<)
≡⟨ ap (fin-pred ^ k) y≡p^lx ⟩
(fin-pred ^ k) ((fin-pred ^ l) ((x , x<n)))
≡⟨ app-comm₃ fin-pred k l _ ⟩
(fin-pred ^ l) ((fin-pred ^ k) (x , x<n))
≡⟨ ap (fin-pred ^ l) p ⟩
(fin-pred ^ l) (x , x<n)
≡⟨ ! y≡p^lx ⟩
(y , y<)
∎
where
find-l : ∑ ℕ (\l → (y +ₙ l ≡ x) × ((0 < l)))
find-l = find-x-to-< y<x
l : ℕ
l = proj₁ find-l
l≡ : y +ₙ l ≡ x
l≡ = proj₁ (proj₂ find-l)
sol-2 : ∑ ℕ (\o → ((y +ₙ l) +ₙ o ≡ succ n) × (0 < o))
sol-2 rewrite l≡ = find-x-to-< x<n
sol : ℕ
sol = proj₁ sol-2
sol≡ : ((y +ₙ l) +ₙ sol ≡ succ n)
sol≡ = (proj₂ ︔ proj₁) sol-2
sol>0 : 0 < sol
sol>0 = proj₂ (proj₂ sol-2)
y+sol : l +ₙ (y +ₙ sol) ≡ succ n
y+sol = (plus-assoc l y sol) · ap (_+ₙ sol) (plus-comm l y) · sol≡
y+sol>0 : (y +ₙ sol) > 0
y+sol>0 rewrite plus-comm y sol = +>0 {sol}{y} sol>0
l<sucn : l < succ n
l<sucn = +≡-to-< {l}{succ n} ((y +ₙ sol) , y+sol) y+sol>0
y≡p^lx : (y , y<) ≡ (fin-pred ^ l) ((x , x<n))
y≡p^lx = (+ₙ-to-fin-pred (y , y<) ((x , x<n)) l l<sucn l≡)
–
change-base
: ∀ {n : ℕ}{k m : ⟦ n ⟧}
→ π₁ k ≡ π₁ m
→ (a x : ⟦ n ⟧)
→ (fin-pred {n} ^ (π₁ k)) a ≡ a
→ (fin-pred {n} ^ (π₁ m)) x ≡ x
change-base {n}{k}{m} idp a x p
rewrite change-point-fin-pred {n}{π₁ k} {x = a} (π₂ k) p = idp
unique-exp-pred
: ∀ {n : ℕ}
→ (k : ℕ) → (k < n)
→ (k' : ℕ) → (k' < n)
→ (x : ⟦ n ⟧)
→ (fin-pred ^ k) x ≡ (fin-pred {n} ^ k') x
--------------------------------------
→ k ≡ k'
unique-exp-pred 0 _ 0 _ _ _ = idp
unique-exp-pred {0} 0 _ (succ k') k'< _ _ = ⊥-elim (n<0 {ℓ} {n = succ k'} k'<)
unique-exp-pred {(succ n)} 0 q (succ k') k'< x f
= ap proj₁
(begin
(0 , q)
≡⟨ fin-pred^-to-fin-suc^ (zero , ∗) (zero , ∗) (succ k') aux ⟩
(fin-suc ^ (succ k')) (0 , q)
≡⟨ +ₙ-to-fin-suc {(succ n)} _ _ (succ k') k'< idp ⟩
(succ k' , k'<)
∎)
where
aux : (fin-pred {succ n} ^ (succ k')) (zero , ∗) ≡ (zero , ∗)
aux = change-base {succ n}{succ k' , k'<}{succ k' , k'<} idp x (zero , ∗) (! f)
unique-exp-pred {succ n} (succ k) k+< 0 p q f
= ! ap proj₁
(begin
(0 , p)
≡⟨ fin-pred^-to-fin-suc^ (zero , ∗) (zero , ∗) (succ k) aux ⟩
(fin-suc ^ (succ k)) (0 , p)
≡⟨ +ₙ-to-fin-suc {(succ n)} _ _ (succ k) k+< idp ⟩
(succ k , k+<)
∎)
where
aux : (fin-pred {succ n} ^ (succ k)) (zero , ∗) ≡ (zero , ∗)
aux = change-base {succ n}{succ k , k+<}{succ k , k+<} idp q (zero , ∗) f
unique-exp-pred {succ n} (succ k) k+< (succ k') k'+< x p =
ap succ
(unique-exp-pred {succ n} k ((n⁺<k→n<k {n = k}{k = succ n} k+<))
k' ((n⁺<k→n<k {n = k'} k'+<)) x (fin-pred-inj p))
fin-exp-is-unique
: ∀ {n : ℕ}
→ (k k' : ⟦ n ⟧)
→ (x : ⟦ n ⟧)
→ (fin-pred ^ (π₁ k)) x ≡ (fin-pred {n} ^ (π₁ k')) x
→ k ≡ k'
fin-exp-is-unique {n} (k , k<n) (k' , k'<n) x p
= pair= (k≡k' , oo k≡k')
where
k≡k' : k ≡ k'
k≡k' = unique-exp-pred {n} k k<n k' k'<n x p
oo : ∀ (o : k ≡ k') → k<n ≡ k'<n [ (λ m → m < n) / o ]
oo idp = <-prop {n}{k} k<n k'<n
fin-is-unique-fin-pred^
: ∀ {n : ℕ}
→ (k k' : ⟦ n ⟧)
→ fin-pred ^ (π₁ k) ≡ fin-pred {n} ^ (π₁ k')
→ k ≡ k'
fin-is-unique-fin-pred^ {n} k k' p
= pair= (o , oo o)
where
o : π₁ k ≡ π₁ k'
o = (unique-exp-fin-pred (π₁ k) (π₂ k) (π₁ k') (π₂ k') p)
oo : ∀ (o : π₁ k ≡ π₁ k') → π₂ k ≡ π₂ k' [ (λ m → m < n) / o ]
oo idp = <-prop {n}{π₁ k} (π₂ k) (π₂ k')
–
p^a-on-a≡0
: ∀ {n : ℕ}{a : ℕ}
→ (a< : a < succ n)
→ (fin-pred {succ n} ^ a) (a , a<) ≡ (0 , unit )
p^a-on-a≡0 {zero} {zero} a<n = idp
p^a-on-a≡0 {zero} {succ zero} a<n = idp
p^a-on-a≡0 {zero} {succ (succ a)} ()
p^a-on-a≡0 {succ n} {zero} ∗ = idp
p^a-on-a≡0 {succ n} {succ a} a+<n+
= begin fin-pred ((fin-pred ^ a) (succ a , a+<n+))
≡⟨ app-comm fin-pred a (succ a , a+<n+) ⟩
(fin-pred ^ a) (fin-pred (succ a , a+<n+))
≡⟨ ap (fin-pred ^ a) idp ⟩
(fin-pred ^ a) (a , a+<n)
≡⟨ p^a-on-a≡0 {succ n}{a} a+<n ⟩
(0 , unit) ∎
where
a+<n : a < succ (succ n)
a+<n = n⁺<k→n<k {a}{succ (succ n)} a+<n+
p^l0≡b
: ∀ {n l b : ℕ}
→ b +ₙ l ≡ succ n
→ (b<n+ : b < succ n)
→ (fin-pred {succ n} ^ l) (0 , unit) ≡ (b , b<n+)
p^l0≡b {zero} {zero} {succ b} p b<n+
rewrite (plus-runit (succ b))
= ⊥-elim {ℓ}{ℓ} (n<0 {n = b} b<n+)
p^l0≡b {zero} {succ .0} {zero} idp ∗ = idp
p^l0≡b {zero} {succ l} {succ b} p b<n+ = ⊥-elim {ℓ₁ = ℓ}{ℓ} (n<0 {n = b} b<n+)
p^l0≡b {succ n} {zero} {succ b} p b<n+
= ⊥-elim (<-=-→⊥ {succ b}{succ (succ n)} b<n+
((! (plus-runit (succ b))) · (p)))
p^l0≡b {succ n} {succ .(succ n)} {zero} idp ∗ =
begin
fin-pred ((fin-pred ^ (succ n)) (0 , ∗))
≡⟨ ap fin-pred (p^l0≡b {l = succ n}{b = 1} idp ∗) ⟩
fin-pred (fin-suc (zero , unit))
≡⟨ fin-suc︔fin-pred∼id _ ⟩
(zero , unit) ∎
p^l0≡b {succ n} {succ l} {succ b} p b<n+
=
fin-pred ((fin-pred ^ l) (0 , ∗))
≡⟨ app-comm fin-pred l (zero , ∗) ⟩
(fin-pred ^ (l)) (fin-pred (0 , unit))
≡⟨ ap (fin-pred ^ l) idp ⟩
(fin-pred ^ (l)) (succ n , <-succ n)
≡⟨ ! +ₙ-to-fin-pred {succ (succ n)} (succ b , b<n+) (succ n , <-succ n) l
oo o ⟩
succ b , b<n+ ∎
where
o : (succ b) +ₙ l ≡ succ n
o = succ-inj (plus-succ (succ b) l · p)
oo : l < succ (succ n)
oo = <-trans {l}{succ l}{succ (succ n)}(<-succ l)
(+≡-to-< {succ l}{succ (succ n)}
(succ b , (plus-comm (succ l) (succ b) · p)) ∗)
unique-sol-if-exists-with-pred
: {n : ℕ}
→ (x : ⟦ n ⟧)
→ (y : ⟦ n ⟧) → (x ≡ fin-pred y)
→ (y' : ⟦ n ⟧) → (x ≡ fin-pred y')
→ (y ≡ y')
unique-sol-if-exists-with-pred x y x≡y y' x≡y' = fin-pred-inj $ ! x≡y · x≡y'
unique-sol-if-exists-with-suc
: {n : ℕ}
→ (x : ⟦ n ⟧)
→ (y : ⟦ n ⟧) → (x ≡ fin-suc y)
→ (y' : ⟦ n ⟧) → (x ≡ fin-suc y')
→ (y ≡ y')
unique-sol-if-exists-with-suc x y x≡y y' x≡y' = fin-suc-inj $ ! x≡y · x≡y'
𝟚-≃-⟦2⟧
: 𝟚 ℓ ≃ ⟦ 2 ⟧
𝟚-≃-⟦2⟧ = qinv-≃ f (g ,
(λ { (zero , π₄) → idp ; (succ zero , ∗) → idp ; (succ (succ π₃) , π₄) → ⊥-elim (n<0 {ℓ}{n = π₃} π₄)})
, λ { 𝟘₂ → idp ; 𝟙₂ → idp})
where
f = λ { 𝟘₂ → (0 , ∗) ; 𝟙₂ → (1 , ∗)}
g = λ { (zero , ∗) → 𝟘₂ ; (succ _ , _) → 𝟙₂}
I need to use the pingeon hole principle, but that lemma uses another definition.
module _ where
Fin₁ = Fin
Fin₂ = ⟦_⟧₂ {ℓ}
⟦_⟧' = ⟦_⟧₂ {ℓ}
Fin₁→Fin₂
: {n : ℕ}
→ Fin₁ n → Fin₂ n
Fin₁→Fin₂ {n = succ n} (zero , p) = inl ∗
Fin₁→Fin₂ {n = succ n} (succ m , sm<sn) = inr (Fin₁→Fin₂ {n} (m , sm<sn))
Fin₂→Fin₁
: {n : ℕ}
→ Fin₂ n → Fin₁ n
Fin₂→Fin₁ {succ n} (inl ∗) = (zero , ∗)
Fin₂→Fin₁ {succ n} (inr i') = succ (proj₁ i) , proj₂ i
where
i = (Fin₂→Fin₁ i')
private
h1 : ∀ n → (x : ⟦ succ n ⟧₂)
→ Fin₁→Fin₂ (Fin₂→Fin₁ x) ≡ x
h1 n (inl ∗) = idp
h1 (succ n) (inr x) = ap inr (ap Fin₁→Fin₂ uic · h1 n x)
where
uic : (π₁ (Fin₂→Fin₁ x) , π₂ (Fin₂→Fin₁ x)) ≡ (Fin₂→Fin₁ x)
uic = idp
h2 : ∀ n → (x : Fin₁ n) → Fin₂→Fin₁ (Fin₁→Fin₂ x) ≡ x
h2 (succ n) (zero , ∗) = idp
h2 (succ n) (succ m , p)
= pair= ((ap succ (ap proj₁ helper) , <-prop {n = n}{m} _ p))
where
helper : Fin₂→Fin₁ (Fin₁→Fin₂ (m , p)) ≡ (m , p)
helper = h2 n (m , p)
Fin₁≃Fin₂
: (n : ℕ)
--------------------
→ (Fin₁ n) ≃ (Fin₂ n)
Fin₁≃Fin₂ zero = qinv-≃ (λ {(zero , ()) ; (succ _ , ())})
( (λ {()}) , (λ {()}) , λ {(zero , ()) ; (succ _ , ())})
Fin₁≃Fin₂ (succ n) = qinv-≃ (Fin₁→Fin₂ {n = succ n}) (Fin₂→Fin₁ , h1 n , h2 (succ n))
module palomar-principle where
_─_ : ∀ {ℓ : Level} → (A : Type ℓ) (x : A) → Type ℓ
_─_ {ℓ} A x = ∑ A (λ a → ((a ≡ x) → ⊥ ℓ))
e→ : ∀ n → (x : ⟦ succ n ⟧')
--------------------------
→ ⟦ n ⟧' → ⟦ succ n ⟧' ─ x
e→ (succ n) (inl _) y = inr y , λ ()
e→ (succ n) (inr x) (inl _) = inl _ , λ ()
e→ (succ n) (inr x) (inr y)
= (inr (π₁ (e→ n x y))) , λ p → π₂ (e→ n x y) (inr-is-injective p)
e←
: ∀ (n : ℕ) → (x : ⟦ succ n ⟧')
----------------------------
→ (⟦ succ n ⟧' ─ x) → ⟦ n ⟧'
e← 0 (inl ∗) (inl ∗ , b) = ⊥-elim (b idp)
e← (succ n) (inl _) (inl _ , b) = inl _
e← (succ n) (inr x) (inl _ , π₄) = inl _
e← (succ n) (inl x) (inr y , b) = y
e← (succ n) (inr x) (inr y , inry≠inrx) = inr (e← n x (y , λ y≡x → inry≠inrx (ap inr y≡x)))
e←:>e→
: ∀ (n : ℕ) → (x : ⟦ succ n ⟧')
→ (e← n x) :> (e→ n x) ∼ id
e←:>e→ 0 (inl ∗) (inl ∗ , π₄) = ⊥-elim $ π₄ (ap inl idp)
e←:>e→ (succ n) (inl _) (inl _ , π₄) = ⊥-elim (π₄ (ap inl idp))
e←:>e→ (succ n) (inl _) (inr x₁ , π₄) = pair= (idp , pi-is-prop (λ a x ()) (λ ()) π₄)
e←:>e→ (succ n) (inr (inl _)) (inl _ , π₄) = pair= (idp , pi-is-prop (λ a x ()) (λ ()) π₄)
e←:>e→ (succ n) (inr (inl x)) (inr y , inry≠inrx)
= pair= ((ap inr (ap π₁ helper) , pi-is-prop (λ a → ⊥-is-prop) _ inry≠inrx))
where
helper : _
helper = e←:>e→ n (inl x) (y , λ y≡inlx → inry≠inrx (ap inr y≡inlx))
e←:>e→ (succ n) (inr (inr x)) (inl _ , π₄) = pair= (idp , pi-is-prop (λ a x ()) (λ ()) π₄)
e←:>e→ (succ n) (inr (inr x)) (inr y , inry≠inrx) = pair= (ap inr (ap π₁ helper)
, pi-is-prop (λ a → ⊥-is-prop) _ inry≠inrx)
where
helper : _
helper = e←:>e→ n (inr x) (y , λ y≡inlx → inry≠inrx (ap inr y≡inlx))
e→:>e←
: ∀ (n : ℕ) → (x : ⟦ succ n ⟧')
→ (e→ n x) :> (e← n x) ∼ id
e→:>e← (succ n) (inl ∗) _ = idp
e→:>e← (succ n) (inr x) (inl x₁) = idp
e→:>e← (succ n) (inr x) (inr y)
= ap inr (ap (e← n x) (pair= (idp , pi-is-prop (λ _ → ⊥-is-prop) _ _)) · helper)
where
helper : _
helper = e→:>e← n x y
e
: ∀ (n : ℕ) → (x : ⟦ succ n ⟧')
--------------------------
→ ⟦ n ⟧' ≃ (⟦ succ n ⟧' ─ x)
e 0 (inl x) = qinv-≃ (λ{()}) ((λ { (inl ∗ , π₄) → ⊥-elim (π₄ idp)} )
, (λ {(inl * , π₄) → ⊥-elim (π₄ idp)}) , λ {()})
e (succ n) x = qinv-≃ (e→ (succ n) x) ((e← (succ n) x )
, (e←:>e→ (succ n) x , e→:>e← (succ n) x))
e-is-bijection
: ∀ (n : ℕ) → (x : ⟦ succ n ⟧')
→ isBijection (apply $ e n x)
⟦⟧₂-is-set
(∑-set ⟦⟧₂-is-set
(λ p → pi-is-set (λ _ → 𝟘-is-set)))
e-is-bijection n x
= ≃-to-bijection ⟦⟧₂-is-set (∑-set ⟦⟧₂-is-set
(λ p → pi-is-set (λ _ → 𝟘-is-set))) (e n x)
inv-e-is-bijection
: ∀ (n : ℕ) → (x : ⟦ succ n ⟧')
→ isBijection (apply $ ≃-sym $ e n x)
(∑-set ⟦⟧₂-is-set (λ p → pi-is-set (λ _ → 𝟘-is-set))) ⟦⟧₂-is-set
inv-e-is-bijection n x
= ≃-to-bijection (∑-set ⟦⟧₂-is-set (λ p → pi-is-set (λ _ → 𝟘-is-set))) ⟦⟧₂-is-set (≃-sym $ e n x)
palomar'
: ∀ (n : ℕ) → (f : ⟦ succ n ⟧' → ⟦ n ⟧' )
----------------------------------------
→ ¬ (isInjective f)
palomar' 0 f _ = f (inl unit)
palomar' (succ n) f f-is-inj = palomar' n g g-is-injective
where
h : (⟦ succ (succ n) ⟧' ─ inl unit) → (⟦ succ n ⟧' ─ (f (inl unit)))
h w@(a , b) = (f a , λ b → π₂ w $ f-is-inj b)
h-is-inj : isInjective h
h-is-inj {a₁ , b₁} {(a₂ , b₂)} p
= pair=
(f-is-inj (ap π₁ p) ,
pi-is-prop (λ a x ()) (tr _ (f-is-inj (ap π₁ p)) b₁) b₂)
g : ⟦ succ n ⟧' → ⟦ n ⟧'
g = lemap (e (succ n) (inl ∗)) :> (h :> remap (e n (f (inl ∗))))
g-is-injective : isInjective g
g-is-injective = ∘-injectives-is-injective _ (π₁ $ e-is-bijection _ _) _
(∘-injectives-is-injective _ h-is-inj _ (π₁ $ inv-e-is-bijection _ _))
pigeon-theorem
: ∀ (n m : ℕ)
→ (m < n) → (f : ⟦ n ⟧' → ⟦ m ⟧')
→ ¬ (isInjective f)
pigeon-theorem (succ n) 0 ∗ f f-is-inj = f (inl ∗)
pigeon-theorem (succ n) (succ m) p f f-is-inj
= pigeon-theorem n m (succ-<-inj {n = m} p) g g-is-injective
where
h : (⟦ succ n ⟧' ─ inl unit) → (⟦ succ m ⟧' ─ (f (inl unit)))
h w@(a , b) = (f a , λ b → π₂ w $ f-is-inj b)
h-is-inj : isInjective h
h-is-inj {a₁ , b₁} {(a₂ , b₂)} p
= pair= (f-is-inj (ap π₁ p)
, pi-is-prop (λ a x ()) (tr _ (f-is-inj (ap π₁ p)) b₁) b₂)
g : ⟦ n ⟧' → ⟦ m ⟧'
g = lemap (e n (inl ∗)) :> h :> remap (e m (f (inl ∗)))
g-is-injective : isInjective g
g-is-injective =
∘-injectives-is-injective _ (π₁ $ e-is-bijection _ _) _
(∘-injectives-is-injective _ h-is-inj _
(π₁ $ inv-e-is-bijection _ _))
Fin-inj-aux-≃ : ∀ {n m : ℕ} → n < m → ⟦ m ⟧' ≃ ⟦ n ⟧' → ⊥ ℓ
Fin-inj-aux-≃ {n = n}{m} n<m f-≃ = pigeon-theorem m n n<m (apply f-≃) (proj₁ f-is-bij)
where
open palomar-principle
f = apply f-≃
f-is-bij : isBijection f ⟦⟧₂-is-set ⟦⟧₂-is-set
f-is-bij = rapply (isBijection-≃-isEquiv {A = ⟦ m ⟧'}{⟦ n ⟧'}
⟦⟧₂-is-set ⟦⟧₂-is-set f) (proj₂ f-≃)
Fin-inj-aux : ∀ {n m : ℕ} → n < m → ⟦ m ⟧' ≡ ⟦ n ⟧' → ⊥ ℓ
Fin-inj-aux {n = n}{m} n<m f-≡ = Fin-inj-aux-≃ n<m (idtoeqv f-≡)
where
open import foundations.UnivalenceAxiom using (idtoeqv)
Fin₂-is-inj-≃
: ∀ (n m : ℕ)
→ ⟦ n ⟧' ≃ ⟦ m ⟧'
-----------------
→ n ≡ m
Fin₂-is-inj-≃ n m e
with trichotomy n m
... | inl (inl idp) = idp
... | inl (inr n<m) = ⊥-elim (Fin-inj-aux-≃ n<m (≃-sym e))
... | inr m<n = ⊥-elim (Fin-inj-aux-≃ m<n e)
Fin₂-is-inj
: ∀ (n m : ℕ)
→ ⟦ n ⟧' ≡ ⟦ m ⟧'
-----------------
→ n ≡ m
Fin₂-is-inj n m p = Fin₂-is-inj-≃ n m (idtoeqv p)
where
open import foundations.UnivalenceAxiom using (idtoeqv)
Fin₁-is-inj-≃
: ∀ (n m : ℕ)
→ ⟦ n ⟧ ≃ ⟦ m ⟧
→ n ≡ m
Fin₁-is-inj-≃ n m e = Fin₂-is-inj-≃ n m
(≃-trans (≃-sym (Fin₁≃Fin₂ n))
(≃-trans e (Fin₁≃Fin₂ m)))
Fin₁-is-inj
: ∀ (n m : ℕ)
→ ⟦ n ⟧ ≡ ⟦ m ⟧
---------------
→ n ≡ m
Fin₁-is-inj n m p = Fin₁-is-inj-≃ n m (idtoeqv p)
where
open import foundations.UnivalenceAxiom using (idtoeqv)
(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