diff --git a/src/Realizability/Assembly/Regular/CharLemmaProof.agda b/src/Realizability/Assembly/Regular/CharLemmaProof.agda index d4730e9..4320d76 100644 --- a/src/Realizability/Assembly/Regular/CharLemmaProof.agda +++ b/src/Realizability/Assembly/Regular/CharLemmaProof.agda @@ -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 @@ -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 diff --git a/src/Realizability/Assembly/Regular/Cobase.agda b/src/Realizability/Assembly/Regular/Cobase.agda index a1ad9e8..0716ad8 100644 --- a/src/Realizability/Assembly/Regular/Cobase.agda +++ b/src/Realizability/Assembly/Regular/Cobase.agda @@ -21,139 +21,9 @@ open import Realizability.Assembly.Morphism ca open import Realizability.Assembly.Regular.CharLemma ca open import Realizability.Assembly.BinProducts ca open import Realizability.Assembly.Coequalizers ca +open import Realizability.Assembly.Regular.KernelPairs ca -module ASMKernelPairs {X Y} (xs : Assembly X) (ys : Assembly Y) (f : AssemblyMorphism xs ys) where - - xs⊗xs = xs ⊗ xs - - kernelPairType = Σ[ x ∈ X ] Σ[ x' ∈ X ] f .map x ≡ f .map x' - - kernelPairOb : Assembly kernelPairType - kernelPairOb .isSetX = isSetΣ (xs .isSetX) λ x → isSetΣ (xs .isSetX) (λ x' → isProp→isSet (ys .isSetX _ _)) - kernelPairOb ._⊩_ a (x , x' , fx≡fx') = xs⊗xs ._⊩_ a (x , x') - kernelPairOb .⊩isPropValued a (x , x' , fx≡fx') = xs⊗xs .⊩isPropValued a (x , x') - kernelPairOb .⊩surjective (x , x' , fx≡fx') = xs⊗xs .⊩surjective (x , x') - - k₁ : AssemblyMorphism kernelPairOb xs - k₁ .map (x , x' , fx≡fx') = x - k₁ .tracker = ∣ pr₁ , (λ (x , x' , fx≡fx') r r⊩xx' → r⊩xx' .fst) ∣₁ - - k₂ : AssemblyMorphism kernelPairOb xs - k₂ .map (x , x' , fx≡fx') = x' - k₂ .tracker = ∣ pr₂ , (λ (x , x' , fx≡fx') r r⊩xx' → r⊩xx' .snd) ∣₁ - - k₁⊚f≡k₂⊚f : k₁ ⊚ f ≡ k₂ ⊚ f - k₁⊚f≡k₂⊚f = - AssemblyMorphism≡ _ _ - (funExt λ (x , x' , fx≡fx') - → f .map (k₁ .map (x , x' , fx≡fx')) - ≡⟨ refl ⟩ - f .map x - ≡⟨ fx≡fx' ⟩ - f .map x' - ≡⟨ refl ⟩ - f .map (k₂ .map (x , x' , fx≡fx')) - ∎) - - module KPUnivProp {Z} {zs : Assembly Z} - (l₁ l₂ : AssemblyMorphism zs xs) - (l₁⊚f≡l₂⊚f : l₁ ⊚ f ≡ l₂ ⊚ f) where - - m : AssemblyMorphism zs kernelPairOb - m .map z = l₁ .map z , l₂ .map z , λ i → l₁⊚f≡l₂⊚f i .map z - m .tracker = {!!} - - module _ (! : AssemblyMorphism zs kernelPairOb) - (l₁≡!⊚k₁ : l₁ ≡ ! ⊚ k₁) - (l₂≡!⊚k₂ : l₂ ≡ ! ⊚ k₂) - (z : Z) where - l₁z≡fst! : l₁ .map z ≡ ! .map z .fst - l₁z≡fst! = l₁ .map z - ≡[ i ]⟨ l₁≡!⊚k₁ i .map z ⟩ - k₁ .map (! .map z) - ≡⟨ refl ⟩ - ! .map z .fst - ∎ - l₂z≡sndfst! : l₂ .map z ≡ ! .map z .snd .fst - l₂z≡sndfst! = l₂ .map z - ≡[ i ]⟨ l₂≡!⊚k₂ i .map z ⟩ - k₂ .map (! .map z) - ≡⟨ refl ⟩ - ! .map z .snd .fst - ∎ - - isSet'Y = isSet→isSet' (ys .isSetX) - {- - This is an important proof in the sense that it is slightly cubical. - Recall the definition of a set : X is a set iff ∀ (x y : X) (p q : x ≡ y) → p ≡ q - Notice that this (mainstream) definition of a set can also be conceptualised as - saying that the following square always has a filler (there is a homotopy between p and q) - p - x — — — > y - ‖ ‖ - ‖ ‖ ^ - ‖ ‖ j | - x — — — > y ∙ — > - q i - - always has a filler. - However, for this proof to work we require *all* squares to have a filler. - I'm not sure how this could be done in the HoTT book. - Applying J twice should work, but for some reason, when I tried it, - it did not work. - -} - uglyPathLemma : PathP (λ i → f .map (l₁z≡fst! i) ≡ f .map (l₂z≡sndfst! i)) (λ i → l₁⊚f≡l₂⊚f i .map z) (snd (snd (! .map z))) - uglyPathLemma i j = - isSet'Y - {a₀₀ = f .map (l₁ .map z)} - {a₀₁ = f .map (l₂ .map z)} - (λ k → l₁⊚f≡l₂⊚f k .map z) - {a₁₀ = f .map (! .map z .fst)} - {a₁₁ = f .map (! .map z .snd .fst)} - (! .map z .snd .snd) - (cong (f .map) l₁z≡fst!) - (cong (f .map) l₂z≡sndfst!) - i j - {- This is what I had attempted : - - explicitJ (f .map (l₁ .map z)) -- J₁ ⊢ x - (f .map (l₂ .map z)) -- J₁ ⊢ y - (λ k → l₁⊚f≡l₂⊚f k .map z) -- J₁ ⊢ x ≡ y - (λ l₁⊚fz l₂⊚fz l₁⊚fz≡l₂⊚fz → {!!}) -- J₁ ⊢ P - (explicitJ -- J₁ ⊢ P x x refl - (f .map (! .map z .fst)) -- J₂ ⊢ x - (f .map (! .map z .snd .fst)) -- J₂ ⊢ y - (! .map z .snd .snd) -- J₂ ⊢ x ≡ y - (λ f!zfst f!zsndfst f!zfst≡f!zsndfst → Y) -- J₂ ⊢ P - (ys .isSetX (f .map (l₁ .map z)) - (f .map (! .map z .fst)) - (cong (f .map) l₁z≡fst!) - {!cong (f .map) l₂z≡sndfst!!} i j)) -- J₂ ⊢ P x x refl -} - - uniqueness : ∀ (! : AssemblyMorphism zs kernelPairOb) → ((l₁ ≡ ! ⊚ k₁) × (l₂ ≡ ! ⊚ k₂)) → m ≡ ! - uniqueness ! (l₁≡!⊚k₁ , l₂≡!⊚k₂) = - AssemblyMorphism≡ _ _ - (funExt (λ z → - ΣPathP (l₁z≡fst! ! l₁≡!⊚k₁ l₂≡!⊚k₂ z , - ΣPathP ((l₂z≡sndfst! ! l₁≡!⊚k₁ l₂≡!⊚k₂ z) , uglyPathLemma ! l₁≡!⊚k₁ l₂≡!⊚k₂ z)))) - - open KPUnivProp - kpUnivProp : isPullback ASM (kernelPairCospan ASM f) k₁ k₂ k₁⊚f≡k₂⊚f - kpUnivProp {Z , zs} l₁ l₂ l₁⊚f≡l₂⊚f = - uniqueExists - (m l₁ l₂ l₁⊚f≡l₂⊚f) - ((AssemblyMorphism≡ _ _ (funExt (λ z → refl))) , AssemblyMorphism≡ _ _ (funExt (λ z → refl))) - (λ ! → isProp× (isSetAssemblyMorphism zs xs _ _) (isSetAssemblyMorphism zs xs _ _)) - λ ! eq@(l₁≡!⊚k₁ , l₂≡!⊚k₂) → uniqueness l₁ l₂ l₁⊚f≡l₂⊚f ! eq - - makeKernelPair : KernelPair ASM f - makeKernelPair = record - { pbOb = kernelPairType , kernelPairOb - ; pbPr₁ = k₁ - ; pbPr₂ = k₂ - ; pbCommutes = k₁⊚f≡k₂⊚f - ; univProp = kpUnivProp - } +open ASMKernelPairs open Pullback module PullbackPreservation diff --git a/src/Realizability/Assembly/Regular/KernelPairs.agda b/src/Realizability/Assembly/Regular/KernelPairs.agda new file mode 100644 index 0000000..dbe5b30 --- /dev/null +++ b/src/Realizability/Assembly/Regular/KernelPairs.agda @@ -0,0 +1,148 @@ +{-# OPTIONS --cubical --allow-unsolved-metas #-} +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.HITs.PropositionalTruncation hiding (map) +open import Cubical.Data.Sigma +open import Cubical.Categories.Limits.Pullback +open import Cubical.Categories.Regular.KernelPair +open import Realizability.CombinatoryAlgebra + +module Realizability.Assembly.Regular.KernelPairs {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open import Realizability.Assembly.Base ca +open import Realizability.Assembly.Morphism ca +open import Realizability.Assembly.BinProducts ca +open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a) + +module ASMKernelPairs {X Y} (xs : Assembly X) (ys : Assembly Y) (f : AssemblyMorphism xs ys) where + + xs⊗xs = xs ⊗ xs + + kernelPairType = Σ[ x ∈ X ] Σ[ x' ∈ X ] f .map x ≡ f .map x' + + kernelPairOb : Assembly kernelPairType + kernelPairOb .isSetX = isSetΣ (xs .isSetX) λ x → isSetΣ (xs .isSetX) (λ x' → isProp→isSet (ys .isSetX _ _)) + kernelPairOb ._⊩_ a (x , x' , fx≡fx') = xs⊗xs ._⊩_ a (x , x') + kernelPairOb .⊩isPropValued a (x , x' , fx≡fx') = xs⊗xs .⊩isPropValued a (x , x') + kernelPairOb .⊩surjective (x , x' , fx≡fx') = xs⊗xs .⊩surjective (x , x') + + k₁ : AssemblyMorphism kernelPairOb xs + k₁ .map (x , x' , fx≡fx') = x + k₁ .tracker = ∣ pr₁ , (λ (x , x' , fx≡fx') r r⊩xx' → r⊩xx' .fst) ∣₁ + + k₂ : AssemblyMorphism kernelPairOb xs + k₂ .map (x , x' , fx≡fx') = x' + k₂ .tracker = ∣ pr₂ , (λ (x , x' , fx≡fx') r r⊩xx' → r⊩xx' .snd) ∣₁ + + k₁⊚f≡k₂⊚f : k₁ ⊚ f ≡ k₂ ⊚ f + k₁⊚f≡k₂⊚f = + AssemblyMorphism≡ _ _ + (funExt λ (x , x' , fx≡fx') + → f .map (k₁ .map (x , x' , fx≡fx')) + ≡⟨ refl ⟩ + f .map x + ≡⟨ fx≡fx' ⟩ + f .map x' + ≡⟨ refl ⟩ + f .map (k₂ .map (x , x' , fx≡fx')) + ∎) + + module KPUnivProp {Z} {zs : Assembly Z} + (l₁ l₂ : AssemblyMorphism zs xs) + (l₁⊚f≡l₂⊚f : l₁ ⊚ f ≡ l₂ ⊚ f) where + + m : AssemblyMorphism zs kernelPairOb + m .map z = l₁ .map z , l₂ .map z , λ i → l₁⊚f≡l₂⊚f i .map z + m .tracker = {!!} + + module _ (! : AssemblyMorphism zs kernelPairOb) + (l₁≡!⊚k₁ : l₁ ≡ ! ⊚ k₁) + (l₂≡!⊚k₂ : l₂ ≡ ! ⊚ k₂) + (z : Z) where + l₁z≡fst! : l₁ .map z ≡ ! .map z .fst + l₁z≡fst! = l₁ .map z + ≡[ i ]⟨ l₁≡!⊚k₁ i .map z ⟩ + k₁ .map (! .map z) + ≡⟨ refl ⟩ + ! .map z .fst + ∎ + l₂z≡sndfst! : l₂ .map z ≡ ! .map z .snd .fst + l₂z≡sndfst! = l₂ .map z + ≡[ i ]⟨ l₂≡!⊚k₂ i .map z ⟩ + k₂ .map (! .map z) + ≡⟨ refl ⟩ + ! .map z .snd .fst + ∎ + + isSet'Y = isSet→isSet' (ys .isSetX) + {- + This is an important proof in the sense that it is slightly cubical. + Recall the definition of a set : X is a set iff ∀ (x y : X) (p q : x ≡ y) → p ≡ q + Notice that this (mainstream) definition of a set can also be conceptualised as + saying that the following square always has a filler (there is a homotopy between p and q) + p + x — — — > y + ‖ ‖ + ‖ ‖ ^ + ‖ ‖ j | + x — — — > y ∙ — > + q i + + always has a filler. + However, for this proof to work we require *all* squares to have a filler. + I'm not sure how this could be done in the HoTT book. + Applying J twice should work, but for some reason, when I tried it, + it did not work. + -} + uglyPathLemma : PathP (λ i → f .map (l₁z≡fst! i) ≡ f .map (l₂z≡sndfst! i)) (λ i → l₁⊚f≡l₂⊚f i .map z) (snd (snd (! .map z))) + uglyPathLemma i j = + isSet'Y + {a₀₀ = f .map (l₁ .map z)} + {a₀₁ = f .map (l₂ .map z)} + (λ k → l₁⊚f≡l₂⊚f k .map z) + {a₁₀ = f .map (! .map z .fst)} + {a₁₁ = f .map (! .map z .snd .fst)} + (! .map z .snd .snd) + (cong (f .map) l₁z≡fst!) + (cong (f .map) l₂z≡sndfst!) + i j + {- This is what I had attempted : + + explicitJ (f .map (l₁ .map z)) -- J₁ ⊢ x + (f .map (l₂ .map z)) -- J₁ ⊢ y + (λ k → l₁⊚f≡l₂⊚f k .map z) -- J₁ ⊢ x ≡ y + (λ l₁⊚fz l₂⊚fz l₁⊚fz≡l₂⊚fz → {!!}) -- J₁ ⊢ P + (explicitJ -- J₁ ⊢ P x x refl + (f .map (! .map z .fst)) -- J₂ ⊢ x + (f .map (! .map z .snd .fst)) -- J₂ ⊢ y + (! .map z .snd .snd) -- J₂ ⊢ x ≡ y + (λ f!zfst f!zsndfst f!zfst≡f!zsndfst → Y) -- J₂ ⊢ P + (ys .isSetX (f .map (l₁ .map z)) + (f .map (! .map z .fst)) + (cong (f .map) l₁z≡fst!) + {!cong (f .map) l₂z≡sndfst!!} i j)) -- J₂ ⊢ P x x refl -} + + uniqueness : ∀ (! : AssemblyMorphism zs kernelPairOb) → ((l₁ ≡ ! ⊚ k₁) × (l₂ ≡ ! ⊚ k₂)) → m ≡ ! + uniqueness ! (l₁≡!⊚k₁ , l₂≡!⊚k₂) = + AssemblyMorphism≡ _ _ + (funExt (λ z → + ΣPathP (l₁z≡fst! ! l₁≡!⊚k₁ l₂≡!⊚k₂ z , + ΣPathP ((l₂z≡sndfst! ! l₁≡!⊚k₁ l₂≡!⊚k₂ z) , uglyPathLemma ! l₁≡!⊚k₁ l₂≡!⊚k₂ z)))) + + open KPUnivProp + kpUnivProp : isPullback ASM (kernelPairCospan ASM f) k₁ k₂ k₁⊚f≡k₂⊚f + kpUnivProp {Z , zs} l₁ l₂ l₁⊚f≡l₂⊚f = + uniqueExists + (m l₁ l₂ l₁⊚f≡l₂⊚f) + ((AssemblyMorphism≡ _ _ (funExt (λ z → refl))) , AssemblyMorphism≡ _ _ (funExt (λ z → refl))) + (λ ! → isProp× (isSetAssemblyMorphism zs xs _ _) (isSetAssemblyMorphism zs xs _ _)) + λ ! eq@(l₁≡!⊚k₁ , l₂≡!⊚k₂) → uniqueness l₁ l₂ l₁⊚f≡l₂⊚f ! eq + + makeKernelPair : KernelPair ASM f + makeKernelPair = record + { pbOb = kernelPairType , kernelPairOb + ; pbPr₁ = k₁ + ; pbPr₂ = k₂ + ; pbCommutes = k₁⊚f≡k₂⊚f + ; univProp = kpUnivProp + }