Skip to content

Commit

Permalink
add more stuff to InjectiveTypes.Sigma
Browse files Browse the repository at this point in the history
  • Loading branch information
@martinescardo
martinescardo committed Sep 7, 2023
1 parent fc2c7ec commit d29baf9
Show file tree
Hide file tree
Showing 3 changed files with 178 additions and 49 deletions.
5 changes: 1 addition & 4 deletions source/InjectiveTypes/MathematicalStructures.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -461,11 +461,8 @@ such as the above, form injective types.

\begin{code}

private
variable
𝓥₁ 𝓥₂ : Universe

closure-under-prop-Π-× :
{𝓤 𝓥₁ 𝓥₂ : Universe}
{S₁ : 𝓤 ̇ → 𝓥₁ ̇ } {S₂ : 𝓤 ̇ → 𝓥₂ ̇ }
→ closed-under-prop-Π S₁
→ closed-under-prop-Π S₂
Expand Down
192 changes: 159 additions & 33 deletions source/InjectiveTypes/Sigma.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,6 @@ injectivity from injectivity.)
This should eventually subsume and improve [1], but this work is not
completed yet.

There are currently a couple of problems with this generalization,
including universe levels.

For the moment I am not going to work any further with this (until I
really need it).

For motivation, the reader should check [1].

Two big improvements here are that
Expand All @@ -29,7 +23,8 @@ Two big improvements here are that
[1] InjectiveTypes.MathematicalStructures.

TODO. Rewrite [1] to use retractions rather than equivalences. This
will be not only more general but also shorter.
will be not only more general but also shorter. Or just apply the
result here.

\begin{code}

Expand All @@ -42,7 +37,6 @@ module InjectiveTypes.Sigma
where

private

fe' : Fun-Ext
fe' {𝓤} {𝓥} = fe 𝓤 𝓥

Expand All @@ -64,21 +58,21 @@ private


module _ {X : 𝓤 ̇ }
(S : X → 𝓦 ̇ )
(S : X → 𝓥 ̇ )
(ϕ : aflabby X 𝓦)
where

ρ : (p : Ω 𝓦) (f : p holds → X)
→ S (extension ϕ p f) → ((h : p holds) → S (f h))
ρ p f s h = transport S (extends ϕ p f h) s

ρ-has-section : 𝓤 ⊔ (𝓦 ⁺) ̇
ρ-has-section = (p : Ω 𝓦)
(f : p holds → X)
→ has-section (ρ p f)
Σ-flabiness-sufficient-condition : 𝓤 ⊔ 𝓥 ⊔ (𝓦 ⁺) ̇
Σ-flabiness-sufficient-condition = (p : Ω 𝓦)
(f : p holds → X)
→ has-section (ρ p f)

Σ-is-aflabby : ρ-has-section → aflabby (Σ S) 𝓦
Σ-is-aflabby hs = I
Σ-is-aflabby : Σ-flabiness-sufficient-condition → aflabby (Σ S) 𝓦
Σ-is-aflabby ρ-has-section = I
where
I : aflabby (Σ S) 𝓦
I P P-is-prop ψ = (extension ϕ p f , s) , II
Expand All @@ -96,10 +90,10 @@ module _ {X : 𝓤 ̇ }
g = pr₂ ∘ ψ

σ : ((h : p holds) → S (f h)) → S (extension ϕ p f)
σ = pr₁ (hs p f)
σ = section-of (ρ p f) (ρ-has-section p f)

η : ρ p f ∘ σ ∼ id
η = pr₂ (hs p f)
η = section-equation (ρ p f) (ρ-has-section p f)

s : S (extension ϕ p f)
s = σ g
Expand All @@ -114,7 +108,7 @@ module _ {X : 𝓤 ̇ }
ρ p f (σ g) h ＝⟨ ap (λ - → - h) (η g) ⟩
g h ∎

Σ-ainjective : ρ-has-section → ainjective-type (Σ S) 𝓦 𝓦
Σ-ainjective : Σ-flabiness-sufficient-condition → ainjective-type (Σ S) 𝓦 𝓦
Σ-ainjective = aflabby-types-are-ainjective (Σ S)
∘ Σ-is-aflabby

Expand Down Expand Up @@ -142,44 +136,176 @@ module _ {X : 𝓤 ̇ }
where
I = dfunext fe' (λ h → (T-is-transport (extends ϕ p f h) s)⁻¹)

ρ'-has-section : 𝓤 ⊔ (𝓦 ⁺) ̇
ρ'-has-section = (p : Ω 𝓦)
(f : p holds → X)
→ has-section (ρ' p f)
Σ-flabiness-sufficient-condition' : 𝓤 ⊔ 𝓥 ⊔ (𝓦 ⁺) ̇
Σ-flabiness-sufficient-condition' = (p : Ω 𝓦)
(f : p holds → X)
→ has-section (ρ' p f)

canonical-section-criterion : ρ'-has-section
→ ρ-has-section
canonical-section-criterion : Σ-flabiness-sufficient-condition'
→ Σ-flabiness-sufficient-condition
canonical-section-criterion ρ'-has-section p f =
has-section-closed-under-∼
(ρ' p f)
(ρ p f)
(ρ'-has-section p f)
(ρs-agreement p f)

canonical-section-criterion-converse : ρ-has-section
→ ρ'-has-section
canonical-section-criterion-converse : Σ-flabiness-sufficient-condition
→ Σ-flabiness-sufficient-condition'
canonical-section-criterion-converse ρ-has-section p f =
has-section-closed-under-∼
(ρ p f)
(ρ' p f)
(ρ-has-section p f)
(∼-sym (ρs-agreement p f))

Σ-flabiness-sufficient-condition-× :
{𝓤 𝓥₁ 𝓥₂ 𝓦 : Universe}
{X : 𝓤 ̇ }
(ϕ : aflabby X 𝓦)
{S₁ : X → 𝓥₁ ̇ } {S₂ : X → 𝓥₂ ̇ }
→ Σ-flabiness-sufficient-condition S₁ ϕ
→ Σ-flabiness-sufficient-condition S₂ ϕ
→ Σ-flabiness-sufficient-condition (λ x → S₁ x × S₂ x) ϕ

Σ-flabiness-sufficient-condition-× {𝓤} {𝓥₁} {𝓥₂} {𝓦} {X} ϕ {S₁} {S₂}
ρ₁-has-section ρ₂-has-section = γ
where
S : X → 𝓥₁ ⊔ 𝓥₂ ̇
S x = S₁ x × S₂ x

module _ (p : Ω 𝓦)
(f : p holds → X)
where

σ₁ : ((h : p holds) → S₁ (f h)) → S₁ (extension ϕ p f)
σ₁ = section-of (ρ S₁ ϕ p f) (ρ₁-has-section p f)

σ₂ : ((h : p holds) → S₂ (f h)) → S₂ (extension ϕ p f)
σ₂ = section-of (ρ S₂ ϕ p f) (ρ₂-has-section p f)

σ : ((h : p holds) → S (f h)) → S (extension ϕ p f)
σ α = σ₁ (λ h → pr₁ (α h)) , σ₂ (λ h → pr₂ (α h))

ρσ : ρ S ϕ p f ∘ σ ∼ id
ρσ α = dfunext fe' I
where
α₁ = λ h → pr₁ (α h)
α₂ = λ h → pr₂ (α h)

I : ρ S ϕ p f (σ α) ∼ α
I h =
ρ S ϕ p f (σ α) h ＝⟨ refl ⟩
transport S (e h) (σ₁ α₁ , σ₂ α₂) ＝⟨ II ⟩
transport S₁ (e h) (σ₁ α₁) , transport S₂ (e h) (σ₂ α₂) ＝⟨ refl ⟩
ρ S₁ ϕ p f (σ₁ α₁) h , ρ S₂ ϕ p f (σ₂ α₂) h ＝⟨ III ⟩
α₁ h , α₂ h ＝⟨ refl ⟩
α h ∎
where
e : (h : p holds) → extension ϕ p f ＝ f h
e = extends ϕ p f

II = transport-× S₁ S₂ (e h)
III = ap₂ _,_
(ap (λ - → - h)
(section-equation (ρ S₁ ϕ p f) (ρ₁-has-section p f) α₁))
(ap (λ - → - h)
(section-equation (ρ S₂ ϕ p f) (ρ₂-has-section p f) α₂))

γ : has-section (ρ S ϕ p f)
γ = (σ , ρσ)

open import UF.Subsingletons

Σ-flabiness-sufficient-condition-with-axioms
: {𝓤 𝓥 𝓦 𝓣 : Universe}
{X : 𝓤 ̇ }
(ϕ : aflabby X 𝓦)
(S : X → 𝓣 ̇ )
(ρ-has-section : Σ-flabiness-sufficient-condition S ϕ)
(axioms : (x : X ) → S x → 𝓦 ̇ )
(axioms-are-prop-valued : (x : X) (s : S x) → is-prop (axioms x s))
(axioms-closed-under-extension
: (p : Ω 𝓦 )
(f : p holds → X )
→ (α : (h : p holds) → S (f h))
→ ((h : p holds) → axioms (f h) (α h))
→ axioms (extension ϕ p f)
(section-of (ρ S ϕ p f) (ρ-has-section p f) α))
→ Σ-flabiness-sufficient-condition (λ X → Σ s ꞉ S X , axioms X s) ϕ
Σ-flabiness-sufficient-condition-with-axioms
{𝓤} {𝓥} {𝓦} {𝓣} {X}
ϕ
S
ρ-has-section
axioms
axioms-are-prop-valued
axioms-closed-under-extension = ρₐ-has-section
where
Sₐ : X → 𝓦 ⊔ 𝓣 ̇
Sₐ x = Σ s ꞉ S x , axioms x s

module _ (p : Ω 𝓦)
(f : p holds → X)
where

σ : ((h : p holds) → S (f h)) → S (extension ϕ p f)
σ = section-of (ρ S ϕ p f) (ρ-has-section p f)

ρₐ : Sₐ (extension ϕ p f) → ((h : p holds) → Sₐ (f h))
ρₐ = ρ Sₐ ϕ p f

σₐ : ((h : p holds) → Sₐ (f h)) → Sₐ (extension ϕ p f)
σₐ α = σ (λ h → pr₁ (α h)) ,
axioms-closed-under-extension p f
(λ h → pr₁ (α h))
(λ h → pr₂ (α h))

ρσₐ : ρₐ ∘ σₐ ∼ id
ρσₐ α = dfunext fe' I
where
α₁ = λ h → pr₁ (α h)
α₂ = λ h → pr₂ (α h)

I : ρₐ (σₐ α) ∼ α
I h =
ρₐ (σₐ α) h ＝⟨ refl ⟩
ρₐ (σ α₁ , _) h ＝⟨ refl ⟩
transport Sₐ (e h) (σ α₁ , _) ＝⟨ II ⟩
(transport S (e h) (σ α₁) , _) ＝⟨ refl ⟩
(ρ S ϕ p f (σ α₁) h , _) ＝⟨ III ⟩
(α₁ h , α₂ h) ＝⟨ refl ⟩
α h ∎
where
e : (h : p holds) → extension ϕ p f ＝ f h
e = extends ϕ p f

II = transport-Σ S axioms (f h) (e h) (σ α₁)
III = to-subtype-＝
(axioms-are-prop-valued (f h))
(ap (λ - → - h)
(section-equation (ρ S ϕ p f) (ρ-has-section p f) α₁))

ρₐ-has-section : has-section ρₐ
ρₐ-has-section = σₐ , ρσₐ

\end{code}

Discussion. It is easy to prove (TODO) that

ΣΣ-is-aflabby : {X : 𝓤 ̇ }
(A : X → ? ̇ ) (B : (x : X) → A x → ? ̇ )
→ (ϕ : aflabby X ?)
→ (hs : ρ-has-section A ϕ)
→ ρ-has-section (λ ((x , a) : Σ A) → B x a) (Σ-is-aflabby A ϕ hs) -- (*)
→ aflabby (Σ x ꞉ X , Σ a ꞉ A x , B x a) ?
ΣΣ-is-aflabby
: {X : 𝓤 ̇ }
(A : X → ? ̇ ) (B : (x : X) → A x → ? ̇ )
→ (ϕ : aflabby X ?)
→ (hs : ρ-has-section A ϕ)
→ ρ-has-section (λ ((x , a) : Σ A) → B x a) (Σ-is-aflabby A ϕ hs) -- (*)
→ aflabby (Σ x ꞉ X , Σ a ꞉ A x , B x a) ?

where the question marks are universes that Agda should be able to
resolve, or at least give contraints to.

However, the hypothesis (*) will not be very useful in practice,
because it is very complicated to state and check. So a good thing to
do would be to formulate and prove an equivalent condition that would
be easier to work with.
be easier to work with. Or even a weaker condition that is good enough
in practice.
30 changes: 18 additions & 12 deletions source/UF/Retracts.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,22 @@ open import UF.Subsingletons
has-section : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
has-section r = Σ s ꞉ (codomain r → domain r), r ∘ s ∼ id

section-of : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (r : X → Y)
→ has-section r
→ (Y → X)
section-of r (s , rs) = s

section-equation : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (r : X → Y)
→ (h : has-section r)
→ r ∘ section-of r h ∼ id
section-equation r (s , rs) = rs

is-section : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
is-section s = Σ r ꞉ (codomain s → domain s), r ∘ s ∼ id

sections-are-lc : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (s : X → Y)
→ is-section s → left-cancellable s
→ is-section s
→ left-cancellable s
sections-are-lc s (r , rs) {x} {x'} p = (rs x)⁻¹ ∙ ap r p ∙ rs x'

retract_of_ : 𝓤 ̇ → 𝓥 ̇ → 𝓤 ⊔ 𝓥 ̇
Expand All @@ -30,7 +41,8 @@ section : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → retract X of Y → (X → Y)
section (r , s , rs) = s

section-is-section : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (ρ : retract X of Y) → is-section (section ρ)
→ (ρ : retract X of Y)
→ is-section (section ρ)
section-is-section (r , s , rs) = r , rs

retract-condition : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (ρ : retract X of Y)
Expand Down Expand Up @@ -226,7 +238,8 @@ retracts-compose (r , s , rs) (r' , s' , rs') =
fg (₁ , y) = ap (λ - → (₁ , -)) (tu y)

Σ-reindex-retract : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : X → 𝓦 ̇ } (r : Y → X)
→ has-section r → retract (Σ A) of (Σ (A ∘ r))
→ has-section r
→ retract (Σ A) of (Σ (A ∘ r))
Σ-reindex-retract {𝓤} {𝓥} {𝓦} {X} {Y} {A} r (s , rs) = γ , φ , γφ
where
γ : (Σ y ꞉ Y , A (r y)) → Σ A
Expand Down Expand Up @@ -378,17 +391,10 @@ ap-of-section-is-section {𝓤} {𝓥} {X} {Y} s (r , rs) x x' = ρ , ρap
ii = ap (λ - → (rs x) ⁻¹ ∙ - ∙ rs x') (ap-ap s r p)
iii = homotopies-are-natural'' (r ∘ s) id rs {x} {x'} {p}

\end{code}

I would phrase this in terms of fibers, but fiber is defined in UF.Equiv which
imports this file.

\begin{code}

Σ-section-retract : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } (ρ : Y ◁ Z) (g : X → Y)
→ (y : Y)
→ (Σ x ꞉ X , g x ＝ y)
◁ (Σ x ꞉ X , section ρ (g x) ＝ section ρ y)
→ fiber g y
◁ fiber (section ρ ∘ g) (section ρ y)
Σ-section-retract {𝓤} {𝓥} {𝓦} {X} {Y} {Z} (r , s , rs) g y =
Σ-retract (λ x → g x ＝ y) (λ x → s (g x) ＝ s y) γ
where
Expand Down

0 comments on commit d29baf9

Please sign in to comment.