Skip to content

Commit

Permalink
Char lemma proof
Browse files Browse the repository at this point in the history
  • Loading branch information
Rahul Chhabra authored and Rahul Chhabra committed Dec 13, 2023
1 parent 9b83179 commit fe46c5c
Show file tree
Hide file tree
Showing 3 changed files with 289 additions and 251 deletions.
258 changes: 139 additions & 119 deletions src/Realizability/Assembly/Regular/CharLemmaProof.agda
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
{-# OPTIONS --cubical --allow-unsolved-metas #-}
open import Realizability.CombinatoryAlgebra
open import Realizability.Choice
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
Expand All @@ -9,132 +10,151 @@ open import Cubical.HITs.PropositionalTruncation hiding (map)
open import Cubical.HITs.PropositionalTruncation.Monad
open import Cubical.Data.Sigma
open import Cubical.Categories.Limits.Coequalizers
open import Cubical.Categories.Regular.Base

module Realizability.Assembly.Regular.CharLemmaProof {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
module Realizability.Assembly.Regular.CharLemmaProof {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) (choice : Choice ℓ ℓ) where

open CombinatoryAlgebra ca
open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
open import Realizability.Assembly.Base ca
open import Realizability.Assembly.Morphism ca
open import Realizability.Assembly.BinProducts ca
open import Realizability.Choice
open import Realizability.Assembly.Regular.CharLemma ca
open import Realizability.Assembly.Regular.KernelPairs ca

module SurjectiveTrackingMakesRegularEpic
{X Y : Type ℓ}
(xs : Assembly X)
(ys : Assembly Y)
(f : AssemblyMorphism xs ys)
(fIsSurjectivelyTracked : isSurjectivelyTracked xs ys f) where

open ASMKernelPairs xs ys f

fIsSurjection : isSurjection (f .map)
fIsSurjection = isSurjectivelyTracked→isSurjective xs ys f fIsSurjectivelyTracked

module _
{Z}
(zs : Assembly Z)
(g : AssemblyMorphism xs zs)
(k₁⊚g≡k₂⊚g : k₁ ⊚ g ≡ k₂ ⊚ g) where

_⊩Z_ = zs ._⊩_

fx≡fx'→gx≡gx' : ∀ x x' → f .map x ≡ f .map x' → g .map x ≡ g .map x'
fx≡fx'→gx≡gx' x x' fx≡fx' i = k₁⊚g≡k₂⊚g i .map (x , x' , fx≡fx')

module _
(h h' : AssemblyMorphism ys zs)
(f⊚h≡q : f ⊚ h ≡ g)
(f⊚h'≡q : f ⊚ h' ≡ g) where
hIsUnique : h ≡ h'
hIsUnique =
AssemblyMorphism≡ _ _
(funExt λ y → equivFun (propTruncIdempotent≃ (zs .isSetX _ _))
(do
(x , fx≡y) ← fIsSurjection y
return (h .map y
≡⟨ sym (cong (λ t → h .map t) fx≡y) ⟩
h .map (f .map x)
≡[ i ]⟨ f⊚h≡q i .map x ⟩
(g .map x)
≡[ i ]⟨ f⊚h'≡q (~ i) .map x ⟩
h' .map (f .map x)
≡⟨ cong (λ t → h' .map t) fx≡y ⟩
h' .map y
∎)))

f⊚h≡gIsProp : isProp (Σ[ h ∈ AssemblyMorphism ys zs ] (f ⊚ h ≡ g))
f⊚h≡gIsProp = λ { (h , e⊚h≡q) (h' , e⊚h'≡q)
→ Σ≡Prop (λ x → isSetAssemblyMorphism xs zs (f ⊚ x) g) (hIsUnique h h' e⊚h≡q e⊚h'≡q ) }

∃h→Σh : ∃[ h ∈ AssemblyMorphism ys zs ] (f ⊚ h ≡ g) → Σ[ h ∈ AssemblyMorphism ys zs ] (f ⊚ h ≡ g)
∃h→Σh ∃h = equivFun (propTruncIdempotent≃ f⊚h≡gIsProp) ∃h

module _
(f⁻¹ : Y → X)
(f⁻¹IsSection : section (f .map) f⁻¹) where

-- I will fix having to do this one day
uglyCalculation : ∀ b g~ r → (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ r) ⨾ Id) ⨾ b) ≡ g~ ⨾ (r ⨾ b)
uglyCalculation b g~ r =
s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ r) ⨾ Id) ⨾ b
≡⟨ sabc≡ac_bc _ _ _ ⟩
k ⨾ g~ ⨾ b ⨾ (s ⨾ (k ⨾ r) ⨾ Id ⨾ b)
≡⟨ cong (λ x → x ⨾ _) (kab≡a _ _) ⟩
g~ ⨾ (s ⨾ (k ⨾ r) ⨾ Id ⨾ b)
≡⟨ cong (λ x → g~ ⨾ x) (sabc≡ac_bc _ _ _) ⟩
g~ ⨾ (k ⨾ r ⨾ b ⨾ (Id ⨾ b))
≡⟨ cong (λ x → g~ ⨾ (x ⨾ (Id ⨾ b))) (kab≡a _ _) ⟩
g~ ⨾ (r ⨾ (Id ⨾ b))
≡⟨ cong (λ x → g~ ⨾ (r ⨾ x)) (Ida≡a _) ⟩
g~ ⨾ (r ⨾ b)
∎

open AssemblyMorphism

module _
{X Y : Type ℓ}
(xs : Assembly X)
(ys : Assembly Y)
(e : AssemblyMorphism xs ys)
where
_⊩X_ = xs ._⊩_
_⊩Y_ = ys ._⊩_
_⊩X×X_ = (xs ⊗ xs) ._⊩_

-- First, isSurjection(e .map) and surjective tracking
-- together create a regular epi in ASM

tracksSurjection : (a : A) → Type ℓ
tracksSurjection a = ∀ y b → (b ⊩Y y) → ∃[ x ∈ X ] (e .map x ≡ y) × ((a ⨾ b) ⊩X x)
module _
(surjection : isSurjection (e .map))
(surjectionIsTracked : ∃[ a ∈ A ] tracksSurjection a)
(choice : Choice ℓ ℓ)
where

kernelType : Type ℓ
kernelType = Σ[ x ∈ X ] Σ[ x' ∈ X ] (e .map x ≡ e .map x')

kernelAssembly : Assembly kernelType
kernelAssembly .isSetX = isSetΣ (xs .isSetX) (λ x → isSetΣ (xs .isSetX) (λ x' → isProp→isSet (ys .isSetX _ _)))
kernelAssembly ._⊩_ r (x , x' , ex≡ex') = (xs ⊗ xs) ._⊩_ r (x , x')
kernelAssembly .⊩isPropValued r (x , x' , ex≡ex') = (xs ⊗ xs) .⊩isPropValued r (x , x')
kernelAssembly .⊩surjective (x , x' , ex≡ex') = (xs ⊗ xs) .⊩surjective (x , x')

-- Kernel Pairs
k₁ : AssemblyMorphism kernelAssembly xs
k₁ .map (x , x' , ex≡ex') = x
k₁ .tracker = ∣ pr₁ , (λ (x , x' , ex≡ex') r r⊩xx' → r⊩xx' .fst) ∣₁
hMap : Y → Z
hMap y = g .map (f⁻¹ y)

fx≡ff⁻¹fx : ∀ x → f .map (f⁻¹ (f .map x)) ≡ f .map x
fx≡ff⁻¹fx x = f⁻¹IsSection (f .map x)

gx≡gf⁻¹fx : ∀ x → g .map (f⁻¹ (f .map x)) ≡ g .map x
gx≡gf⁻¹fx x = fx≡fx'→gx≡gx' (f⁻¹ (f .map x)) x (fx≡ff⁻¹fx x)

hfx≡gx : ∀ x → hMap (f .map x) ≡ g .map x
hfx≡gx x = gx≡gf⁻¹fx x

h : AssemblyMorphism ys zs
h .map y = hMap y
h .tracker =
do
(g~ , g~tracks) ← g .tracker
(r , rWitness) ← fIsSurjectivelyTracked
return
(s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ r) ⨾ Id) ,
(λ y b b⊩y →
equivFun
(propTruncIdempotent≃ (zs .⊩isPropValued _ _))
(do
(x , fx≡y , rb⊩x) ← rWitness y b b⊩y
return
(subst
(λ h~ → h~ ⊩Z (h .map y))
(sym (uglyCalculation b g~ r))
(subst (λ x → (g~ ⨾ (r ⨾ b)) ⊩Z x)
(sym (subst (λ y → hMap y ≡ g .map x) fx≡y (hfx≡gx x)))
(g~tracks x (r ⨾ b) rb⊩x))))))


k₂ : AssemblyMorphism kernelAssembly xs
k₂ .map (x , x' , ex≡ex') = x'
k₂ .tracker = ∣ pr₂ , (λ (x , x' , ex≡ex') r r⊩xx' → r⊩xx' .snd) ∣₁

module _ {W : Type ℓ}
{ws : Assembly W}
(q : AssemblyMorphism xs ws)
(k₁q≡k₂q : k₁ ⊚ q ≡ k₂ ⊚ q) where

module _
(h h' : AssemblyMorphism ys ws)
(e⊚h≡q : e ⊚ h ≡ q)
(e⊚h'≡q : e ⊚ h' ≡ q) where
hIsUnique : h ≡ h'
hIsUnique =
AssemblyMorphism≡ _ _
(funExt λ y → equivFun (propTruncIdempotent≃ (ws .isSetX _ _))
(do
(x , ex≡y) ← surjection y
return (h .map y
≡⟨ sym (cong (λ t → h .map t) ex≡y) ⟩
h .map (e .map x)
≡[ i ]⟨ e⊚h≡q i .map x ⟩
(q .map x)
≡[ i ]⟨ e⊚h'≡q (~ i) .map x ⟩
h' .map (e .map x)
≡⟨ cong (λ t → h' .map t) ex≡y ⟩
h' .map y
∎)))

e⊚t≡qIsProp : isProp (Σ[ t ∈ AssemblyMorphism ys ws ] (e ⊚ t ≡ q))
e⊚t≡qIsProp = λ { (h , e⊚h≡q) (h' , e⊚h'≡q)
→ Σ≡Prop (λ x → isSetAssemblyMorphism xs ws (e ⊚ x) q) (hIsUnique h h' e⊚h≡q e⊚h'≡q ) }

∃t→Σt : ∃[ t ∈ AssemblyMorphism ys ws ] (e ⊚ t ≡ q) → Σ[ t ∈ AssemblyMorphism ys ws ] (e ⊚ t ≡ q)
∃t→Σt ∃t = equivFun (propTruncIdempotent≃ e⊚t≡qIsProp) ∃t

-- I have cooked one ugly proof ngl 😀🔫
open IsCoequalizer
eIsCoequalizer : IsCoequalizer {C = ASM} k₁ k₂ e
eIsCoequalizer .glues = AssemblyMorphism≡ _ _ (funExt λ (x , x' , ex≡ex') → ex≡ex')
eIsCoequalizer .univProp {W , ws} q k₁q≡k₂q =
uniqueExists
(∃t→Σt q k₁q≡k₂q ∃t .fst)
(∃t→Σt q k₁q≡k₂q ∃t .snd)
(λ t → isSetAssemblyMorphism _ _ _ _)
λ t e⊚t≡q → λ i → e⊚t≡qIsProp q k₁q≡k₂q (∃t→Σt q k₁q≡k₂q ∃t) (t , e⊚t≡q) i .fst where
_⊩W_ = ws ._⊩_
∃t : ∃[ t ∈ AssemblyMorphism ys ws ] (e ⊚ t ≡ q)
∃t = (do
(e⁻¹ , e⁻¹IsSection) ← choice X Y (xs .isSetX) (ys .isSetX) (e .map) surjection
return (h e⁻¹ e⁻¹IsSection , {!!})) where
module _
(e⁻¹ : Y → X)
(e⁻¹IsSection : section (e .map) e⁻¹) where
h : AssemblyMorphism ys ws
h .map y = q .map (e⁻¹ y)
h .tracker =
do
(q~ , q~tracks) ← q .tracker
(r , rWitness) ← surjectionIsTracked
return (s ⨾ (k ⨾ q~) ⨾ (s ⨾ (k ⨾ r) ⨾ Id) , (λ y b b⊩y → {!!}))

e⊚h≡q : e ⊚ h ≡ q
e⊚h≡q = AssemblyMorphism≡ _ _
(funExt λ x →
h .map (e .map x)
≡⟨ refl ⟩
q .map (e⁻¹ (e .map x))
≡⟨ {!(e⁻¹IsSection (e .map x))!} ⟩
q .map x
∎)

hy≡qx : ∀ x y → e .map x ≡ y → h .map y ≡ q .map x
hy≡qx x y ex≡y =
h .map y
≡⟨ refl ⟩
q .map (e⁻¹ y)
≡⟨ {!e⁻¹IsSection (e .map x)!} ⟩
q .map x
∎

f⊚h≡g : f ⊚ h ≡ g
f⊚h≡g = AssemblyMorphism≡ _ _ (funExt λ x → hfx≡gx x)

∃h : ∃[ h ∈ AssemblyMorphism ys zs ] (f ⊚ h ≡ g)
∃h =
do
(f⁻¹ , f⁻¹IsSection) ← choice X Y (xs .isSetX) (ys .isSetX) (f .map) fIsSurjection
return (h f⁻¹ f⁻¹IsSection , f⊚h≡g f⁻¹ f⁻¹IsSection)

Σh : Σ[ h ∈ AssemblyMorphism ys zs ] (f ⊚ h ≡ g)
Σh = ∃h→Σh ∃h

kernelPairCoeqUnivProp : ∀ {Z} {zs : Assembly Z} → (g : AssemblyMorphism xs zs) → (k₁ ⊚ g ≡ k₂ ⊚ g) → ∃![ ! ∈ AssemblyMorphism ys zs ] (f ⊚ ! ≡ g)
kernelPairCoeqUnivProp {Z} {zs} g k₁⊚g≡k₂⊚g =
uniqueExists
(Σh zs g k₁⊚g≡k₂⊚g .fst)
(Σh zs g k₁⊚g≡k₂⊚g .snd)
(λ ! → isSetAssemblyMorphism _ _ _ _)
λ ! f⊚!≡g → hIsUnique zs g k₁⊚g≡k₂⊚g (Σh zs g k₁⊚g≡k₂⊚g .fst) ! (Σh zs g k₁⊚g≡k₂⊚g .snd) f⊚!≡g

kernelPairCoequalizer : IsCoequalizer {C = ASM} k₁ k₂ f
kernelPairCoequalizer = record { glues = k₁⊚f≡k₂⊚f ; univProp = λ q qGlues → kernelPairCoeqUnivProp q qGlues }

isRegularEpicASMe : isRegularEpic ASM f
isRegularEpicASMe = ∣ (kernelPairType , kernelPairOb) , ∣ k₁ , ∣ k₂ , kernelPairCoequalizer ∣₁ ∣₁ ∣₁

open SurjectiveTrackingMakesRegularEpic

charLemmaProof : CharLemma
charLemmaProof = λ xs ys e → (λ eIsRegular → {!!}) , λ eIsSurjectivelyTracked → isRegularEpicASMe xs ys e eIsSurjectivelyTracked
Loading

0 comments on commit fe46c5c

Please sign in to comment.