From 41d4f1856b036394e31e3a7805aea014dca3d1b0 Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Tue, 25 Jun 2024 19:34:12 +0530 Subject: [PATCH] Finite Limits for PERs --- .../Assembly/LocallyCartesianClosed.agda | 70 ++--- src/Realizability/Modest/UniformFamily.agda | 2 + src/Realizability/PERs/BinProducts.agda | 196 ++++++++++++++ src/Realizability/PERs/PER.agda | 240 +++++++++--------- src/Realizability/PERs/TerminalObject.agda | 12 +- src/Utils/SQElim.agda | 52 ++++ 6 files changed, 395 insertions(+), 177 deletions(-) create mode 100644 src/Realizability/PERs/BinProducts.agda create mode 100644 src/Utils/SQElim.agda diff --git a/src/Realizability/Assembly/LocallyCartesianClosed.agda b/src/Realizability/Assembly/LocallyCartesianClosed.agda index 669ce5f..81b0170 100644 --- a/src/Realizability/Assembly/LocallyCartesianClosed.agda +++ b/src/Realizability/Assembly/LocallyCartesianClosed.agda @@ -270,63 +270,27 @@ module _ {X Y : Type ℓ} {asmX : Assembly X} {asmY : Assembly Y} (f : AssemblyM (sym (λ*ComputationRule realizer a)) (isTrackedH v (pr₂ ⨾ a) pr₂a⊩v .snd (x , sym (isFiberOfY x v fx≡gv)) (pr₁ ⨾ a) pr₁a⊩x) })) + opaque + unfolding pullback + unfolding answer + unfolding answerMap + answerEq : answer ⊚ m ≡ (reindexFunctor ASM PullbacksASM f ⟅ sliceob g ⟆) .S-arr + answerEq = + AssemblyMorphism≡ _ _ + (funExt + λ { q@(x , v , fx≡gv) → + m .map (answerMap q) + ≡⟨ refl ⟩ + m .map (h .map v .fst .snd .fst (x , sym (isFiberOfY x v fx≡gv))) + ≡⟨ h .map v .fst .snd .snd (x , sym (isFiberOfY x v fx≡gv)) ⟩ + x + ∎ }) + opaque unfolding pullback reindex⊣Π[_] : reindexFunctor ASM PullbacksASM f ⊣ Π[_] Iso.fun (_⊣_.adjIso reindex⊣Π[_] {sliceob {V , asmV} g} {sliceob {P , asmP} m}) (slicehom h hComm) = slicehom (ForwardIso.answer g m h hComm) (ForwardIso.answerEq g m h hComm) - Iso.inv (_⊣_.adjIso reindex⊣Π[_] {sliceob {V , asmV} g} {sliceob {P , asmP} m}) (slicehom h hComm) = - slicehom answer (AssemblyMorphism≡ _ _ (funExt λ { (x , v , fx≡gv) → answerEq x v fx≡gv })) where - Π[f]m : AssemblyMorphism (S-ob (Π[_] ⟅ sliceob m ⟆) .snd) asmY - Π[f]m = (Π[_] ⟅ sliceob m ⟆) .S-arr - - Q : ASM .Category.ob - Q = (reindexFunctor ASM PullbacksASM f ⟅ sliceob g ⟆) .S-ob - - typeQ : Type ℓ - typeQ = Q .fst - - asmQ : Assembly typeQ - asmQ = Q .snd - - isFiberOfY : (x : X) → (v : V) → f .map x ≡ g .map v → h .map v .fst .fst ≡ f .map x - isFiberOfY x v fx≡gv = - h .map v .fst .fst - ≡[ i ]⟨ hComm i .map v ⟩ - g .map v - ≡⟨ sym fx≡gv ⟩ - f .map x - ∎ - - answerMap : typeQ → P - answerMap (x , v , fx≡gv) = - h .map v .fst .snd .fst - (x , - sym (isFiberOfY x v fx≡gv)) - - answerEq : (x : X) (v : V) (fx≡gv : f .map x ≡ g .map v) → m .map (answerMap (x , v , fx≡gv)) ≡ x - answerEq x v fx≡gv = - m .map (answerMap (x , v , fx≡gv)) - ≡⟨ refl ⟩ - m .map (h .map v .fst .snd .fst (x , sym (isFiberOfY x v fx≡gv))) - ≡⟨ h .map v .fst .snd .snd (x , sym (isFiberOfY x v fx≡gv)) ⟩ - x - ∎ - - answer : AssemblyMorphism asmQ asmP - AssemblyMorphism.map answer = answerMap - AssemblyMorphism.tracker answer = - do - (h~ , isTrackedH) ← h .tracker - let - realizer : Term as 1 - realizer = ` pr₂ ̇ (` h~ ̇ (` pr₂ ̇ # zero)) ̇ (` pr₁ ̇ # zero) - return - (λ* realizer , - (λ { q@(x , v , fx≡gv) a (pr₁a⊩x , pr₂a⊩v) → - subst - (λ r' → r' ⊩[ asmP ] (answerMap (x , v , fx≡gv))) - (sym (λ*ComputationRule realizer a)) - (isTrackedH v (pr₂ ⨾ a) pr₂a⊩v .snd (x , sym (isFiberOfY x v fx≡gv)) (pr₁ ⨾ a) pr₁a⊩x) })) + Iso.inv (_⊣_.adjIso reindex⊣Π[_] {sliceob {V , asmV} g} {sliceob {P , asmP} m}) (slicehom h hComm) = slicehom (BackwardIso.answer g m h hComm) (BackwardIso.answerEq g m h hComm) Iso.rightInv (_⊣_.adjIso reindex⊣Π[_] {sliceob {V , asmV} g} {sliceob {P , asmP} m}) (slicehom h hComm) = SliceHom-≡-intro' ASM diff --git a/src/Realizability/Modest/UniformFamily.agda b/src/Realizability/Modest/UniformFamily.agda index 8dfb38a..805446a 100644 --- a/src/Realizability/Modest/UniformFamily.agda +++ b/src/Realizability/Modest/UniformFamily.agda @@ -65,5 +65,7 @@ Categoryᴰ.⋆Assocᴰ UNIMOD ΣPathPProp (λ comp → isSetAssemblyMorphism asmXᴰ asmW _ _) (Category.⋆Assoc ASM fᵈ gᵈ hᵈ ) Categoryᴰ.isSetHomᴰ UNIMOD = isSetΣ (isSetAssemblyMorphism _ _) (λ f → isProp→isSet (isSetAssemblyMorphism _ _ _ _)) +open Categoryᴰ UNIMOD + UniformFamily : {X : Type ℓ} → (asmX : Assembly X) → Type (ℓ-suc ℓ) UniformFamily {X} asmX = UNIMOD .Categoryᴰ.ob[_] (X , asmX) diff --git a/src/Realizability/PERs/BinProducts.agda b/src/Realizability/PERs/BinProducts.agda new file mode 100644 index 0000000..0f9ae26 --- /dev/null +++ b/src/Realizability/PERs/BinProducts.agda @@ -0,0 +1,196 @@ +open import Realizability.ApplicativeStructure +open import Realizability.CombinatoryAlgebra +open import Realizability.PropResizing +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Structure using (⟨_⟩; str) +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Powerset +open import Cubical.Functions.FunExtEquiv +open import Cubical.Relation.Binary +open import Cubical.Data.Sigma +open import Cubical.Data.FinData +open import Cubical.Data.Unit +open import Cubical.Reflection.RecordEquiv +open import Cubical.HITs.PropositionalTruncation as PT hiding (map) +open import Cubical.HITs.PropositionalTruncation.Monad +open import Cubical.HITs.SetQuotients as SQ +open import Cubical.Categories.Category +open import Cubical.Categories.Limits.BinProduct +open import Utils.SQElim as SQElim + +module Realizability.PERs.BinProducts + {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where + +open import Realizability.PERs.PER ca +open CombinatoryAlgebra ca +open Combinators ca renaming (i to Id; ia≡a to Ida≡a) +open PER +open Category PERCat + +module _ (R S : PER) where + binProdObPER : PER + PER.relation binProdObPER = + (λ a b → (pr₁ ⨾ a) ~[ R ] (pr₁ ⨾ b) × (pr₂ ⨾ a) ~[ S ] (pr₂ ⨾ b)) , λ a b → isProp× (isProp~ (pr₁ ⨾ a) R (pr₁ ⨾ b)) (isProp~ (pr₂ ⨾ a) S (pr₂ ⨾ b)) + fst (isPER binProdObPER) a b (pr₁a~[R]pr₁b , pr₂a~[S]pr₂b) = + (isSymmetric R (pr₁ ⨾ a) (pr₁ ⨾ b) pr₁a~[R]pr₁b) , (isSymmetric S (pr₂ ⨾ a) (pr₂ ⨾ b) pr₂a~[S]pr₂b) + snd (isPER binProdObPER) a b c (pr₁a~[R]pr₁b , pr₂a~[S]pr₂b) (pr₁b~[R]pr₁c , pr₂b~[S]pr₂c) = + (isTransitive R (pr₁ ⨾ a) (pr₁ ⨾ b) (pr₁ ⨾ c) pr₁a~[R]pr₁b pr₁b~[R]pr₁c) , (isTransitive S (pr₂ ⨾ a) (pr₂ ⨾ b) (pr₂ ⨾ c) pr₂a~[S]pr₂b pr₂b~[S]pr₂c) + + isTrackerPr₁ : isTracker binProdObPER R pr₁ + isTrackerPr₁ = λ r r' (pr₁r~[R]pr₁r' , pr₂r~[S]pr₂r') → pr₁r~[R]pr₁r' + + binProdPr₁Tracker : perTracker binProdObPER R + binProdPr₁Tracker = pr₁ , isTrackerPr₁ + + binProdPr₁PER : perMorphism binProdObPER R + binProdPr₁PER = [ binProdPr₁Tracker ] + + isTrackerPr₂ : isTracker binProdObPER S pr₂ + isTrackerPr₂ = λ { r r' (pr₁r~[R]pr₁r' , pr₂r~[S]pr₂r') → pr₂r~[S]pr₂r' } + + binProdPr₂Tracker : perTracker binProdObPER S + binProdPr₂Tracker = pr₂ , isTrackerPr₂ + + binProdPr₂PER : perMorphism binProdObPER S + binProdPr₂PER = [ binProdPr₂Tracker ] + + binProdUnivPropPER : + (T : PER) + (f : perMorphism T R) + (g : perMorphism T S) → + ∃![ ! ∈ perMorphism T binProdObPER ] ((composePerMorphism T binProdObPER R ! binProdPr₁PER ≡ f) × (composePerMorphism T binProdObPER S ! binProdPr₂PER ≡ g)) + binProdUnivPropPER T f g = + inhProp→isContr + map + (isPropMapType f g) where + + mapEqProj1 : ∀ ! f' → Type _ + mapEqProj1 ! f' = composePerMorphism T binProdObPER R ! binProdPr₁PER ≡ f' + + mapEqProj2 : ∀ ! g' → Type _ + mapEqProj2 ! g' = composePerMorphism T binProdObPER S ! binProdPr₂PER ≡ g' + + mapEqs : ∀ ! f' g' → Type _ + mapEqs ! f' g' = (composePerMorphism T binProdObPER R ! binProdPr₁PER ≡ f') × (composePerMorphism T binProdObPER S ! binProdPr₂PER ≡ g') + + isPropMapEqs : ∀ ! f' g' → isProp (mapEqs ! f' g') + isPropMapEqs ! f' g' = isProp× (squash/ _ _) (squash/ _ _) + + mapType : ∀ f' g' → Type _ + mapType f' g' = Σ[ ! ∈ perMorphism T binProdObPER ] (mapEqs ! f' g') + + mapRealizer : ∀ a b → Term as 1 + mapRealizer a b = ` pair ̇ (` a ̇ # zero) ̇ (` b ̇ # zero) + + isSetMapType : ∀ f' g' → isSet (mapType f' g') + isSetMapType f' g' = isSetΣ squash/ (λ ! → isSet× (isProp→isSet (squash/ _ _)) (isProp→isSet (squash/ _ _))) + + isPropMapType : ∀ f' g' → isProp (mapType f' g') + isPropMapType f' g' (! , !⋆π₁≡f , !⋆π₂≡g) (!' , !'⋆π₁≡f , !'⋆π₂≡g) = + Σ≡Prop + (λ ! → isPropMapEqs ! f' g') + (SQ.elimProp4 + {P = motive} + isPropMotive + goal + f' g' ! !' + !⋆π₁≡f + !⋆π₂≡g + !'⋆π₁≡f + !'⋆π₂≡g) where + + motive : ∀ f' g' ! !' → Type _ + motive f' g' ! !' = ∀ (!proj1 : mapEqProj1 ! f') (!proj2 : mapEqProj2 ! g') (!'proj1 : mapEqProj1 !' f') (!'proj2 : mapEqProj2 !' g') → ! ≡ !' + + isPropMotive : ∀ f' g' ! !' → isProp (motive f' g' ! !') + isPropMotive f' g' ! !' = + isPropΠ4 λ _ _ _ _ → squash/ _ _ + + goal : ∀ f' g' ! !' → motive [ f' ] [ g' ] [ ! ] [ !' ] + goal (f , f⊩f) (g , g⊩g) (a , a⊩!) (b , b⊩!') !proj1 !proj2 !'proj1 !'proj2 = + eq/ _ _ + λ r r~r → + let + pr₁Equiv : (pr₁ ⨾ (a ⨾ r)) ~[ R ] (pr₁ ⨾ (b ⨾ r)) + pr₁Equiv = + isTransitive + R (pr₁ ⨾ (a ⨾ r)) (f ⨾ r) (pr₁ ⨾ (b ⨾ r)) + (subst (_~[ R ] (f ⨾ r)) (λ*ComputationRule (` pr₁ ̇ (` a ̇ # zero)) r) (!proj1Equiv r r~r)) + (isSymmetric R (pr₁ ⨾ (b ⨾ r)) (f ⨾ r) (subst (_~[ R ] (f ⨾ r)) (λ*ComputationRule (` pr₁ ̇ (` b ̇ # zero)) r) (!'proj1Equiv r r~r))) + + pr₂Equiv : (pr₂ ⨾ (a ⨾ r)) ~[ S ] (pr₂ ⨾ (b ⨾ r)) + pr₂Equiv = + isTransitive + S (pr₂ ⨾ (a ⨾ r)) (g ⨾ r) (pr₂ ⨾ (b ⨾ r)) + (subst (_~[ S ] (g ⨾ r)) (λ*ComputationRule (` pr₂ ̇ (` a ̇ # zero)) r) (!proj2Equiv r r~r)) + (isSymmetric S (pr₂ ⨾ (b ⨾ r)) (g ⨾ r) (subst (_~[ S ] (g ⨾ r)) (λ*ComputationRule (` pr₂ ̇ (` b ̇ # zero)) r) (!'proj2Equiv r r~r))) + in + pr₁Equiv , + pr₂Equiv where + !proj1Equiv : isEquivTracker T R (composePerTracker T binProdObPER R (a , a⊩!) binProdPr₁Tracker) (f , f⊩f) + !proj1Equiv = effectiveIsEquivTracker T R _ _ !proj1 + + !proj2Equiv : isEquivTracker T S (composePerTracker T binProdObPER S (a , a⊩!) binProdPr₂Tracker) (g , g⊩g) + !proj2Equiv = effectiveIsEquivTracker T S _ _ !proj2 + + !'proj1Equiv : isEquivTracker T R (composePerTracker T binProdObPER R (b , b⊩!') binProdPr₁Tracker) (f , f⊩f) + !'proj1Equiv = effectiveIsEquivTracker T R _ _ !'proj1 + + !'proj2Equiv : isEquivTracker T S (composePerTracker T binProdObPER S (b , b⊩!') binProdPr₂Tracker) (g , g⊩g) + !'proj2Equiv = effectiveIsEquivTracker T S _ _ !'proj2 + + coreMap : ∀ a b → mapType [ a ] [ b ] + coreMap (a , a⊩f) (b , b⊩g) = + [ (λ* (mapRealizer a b)) , + (λ r r' r~r' → + subst2 + (λ abr abr' → abr ~[ binProdObPER ] abr') + (sym (λ*ComputationRule (mapRealizer a b) r)) + (sym (λ*ComputationRule (mapRealizer a b) r')) + (subst2 + (λ ar ar' → ar ~[ R ] ar') + (sym (pr₁pxy≡x _ _)) + (sym (pr₁pxy≡x _ _)) + (a⊩f r r' r~r') , + subst2 + (λ br br' → br ~[ S ] br') + (sym (pr₂pxy≡y _ _)) + (sym (pr₂pxy≡y _ _)) + (b⊩g r r' r~r'))) ] , + eq/ _ _ + (λ r r~r → + subst + (_~[ R ] (a ⨾ r)) + (sym + (λ*ComputationRule (` pr₁ ̇ (` λ* (mapRealizer a b) ̇ # zero)) r ∙ + cong (pr₁ ⨾_) (λ*ComputationRule (mapRealizer a b) r))) + (subst (_~[ R ] (a ⨾ r)) (sym (pr₁pxy≡x _ _)) (a⊩f r r r~r))) , + eq/ _ _ + λ r r~r → + subst + (_~[ S ] (b ⨾ r)) + (sym + (λ*ComputationRule (` pr₂ ̇ (` λ* (mapRealizer a b) ̇ # zero)) r ∙ + cong (pr₂ ⨾_) (λ*ComputationRule (mapRealizer a b) r) ∙ + pr₂pxy≡y _ _)) + (b⊩g r r r~r) + + map : mapType f g + map = + SQ.elimProp2 + {P = mapType} + isPropMapType + coreMap + f g + +BinProductPER : (R S : PER) → BinProduct PERCat R S +BinProduct.binProdOb (BinProductPER R S) = binProdObPER R S +BinProduct.binProdPr₁ (BinProductPER R S) = binProdPr₁PER R S +BinProduct.binProdPr₂ (BinProductPER R S) = binProdPr₂PER R S +BinProduct.univProp (BinProductPER R S) {T} f g = binProdUnivPropPER R S T f g + +BinProductsPER : BinProducts PERCat +BinProductsPER R S = BinProductPER R S diff --git a/src/Realizability/PERs/PER.agda b/src/Realizability/PERs/PER.agda index bd5adb7..90ca204 100644 --- a/src/Realizability/PERs/PER.agda +++ b/src/Realizability/PERs/PER.agda @@ -12,6 +12,7 @@ open import Cubical.Functions.FunExtEquiv open import Cubical.Relation.Binary open import Cubical.Data.Sigma open import Cubical.Data.FinData +open import Cubical.Data.Vec open import Cubical.Reflection.RecordEquiv open import Cubical.HITs.PropositionalTruncation as PT hiding (map) open import Cubical.HITs.PropositionalTruncation.Monad @@ -52,126 +53,125 @@ record PER : Type (ℓ-suc ℓ) where open PER -module _ (R : PER) where - Quotient = A / ∣ R ∣ - - -- mimics the proof at Cubical.HITs.SetQuotients.Properties - effectiveOnDomain : ∀ a b → ∣ R ∣ a a → [ a ] ≡ [ b ] → ∣ R ∣ a b - effectiveOnDomain a b aRa [a]≡[b] = transport aRa≡aRb aRa where - helper : Quotient → hProp _ - helper x = - SQ.rec - isSetHProp - (λ c → (∣ R ∣ a c) , (isPropValued R a c)) - (λ c d cRd → - Σ≡Prop - (λ _ → isPropIsProp) - (hPropExt - (isPropValued R a c) - (isPropValued R a d) - (λ aRc → isTransitive R a c d aRc cRd) - (λ aRd → isTransitive R a d c aRd (isSymmetric R c d cRd)))) - x - - aRa≡aRb : ∣ R ∣ a a ≡ ∣ R ∣ a b - aRa≡aRb i = helper ([a]≡[b] i) .fst - -record PERMorphism (R S : PER) : Type ℓ where - no-eta-equality - constructor makePERMorphism - field - map : Quotient R → Quotient S - isTracked : ∃[ e ∈ A ] (∀ (a : A) → ∣ R ∣ a a → (map [ a ] ≡ [ e ⨾ a ]) × ∣ S ∣ (e ⨾ a) (e ⨾ a)) - -open PERMorphism - -unquoteDecl PERMorphismIsoΣ = declareRecordIsoΣ PERMorphismIsoΣ (quote PERMorphism) - -PERMorphismΣ : PER → PER → Type ℓ -PERMorphismΣ R S = Σ[ map ∈ (Quotient R → Quotient S) ] ∃[ e ∈ A ] (∀ (a : A) → ∣ R ∣ a a → (map [ a ] ≡ [ e ⨾ a ]) × ∣ S ∣ (e ⨾ a) (e ⨾ a)) - -isSetPERMorphismΣ : ∀ {R S} → isSet (PERMorphismΣ R S) -isSetPERMorphismΣ {R} {S} = isSetΣ (isSet→ squash/) (λ map → isProp→isSet isPropPropTrunc) - -isSetPERMorphism : ∀ {R S} → isSet (PERMorphism R S) -isSetPERMorphism {R} {S} = subst (λ type → isSet type) (sym (isoToPath PERMorphismIsoΣ)) (isSetPERMorphismΣ {R = R} {S = S}) - -PERMorphism≡Iso : ∀ {R S} → (f g : PERMorphism R S) → Iso (f ≡ g) (f .map ≡ g .map) -Iso.fun (PERMorphism≡Iso {R} {S} f g) f≡g i = f≡g i .map -map (Iso.inv (PERMorphism≡Iso {R} {S} f g) fMap≡gMap i) = fMap≡gMap i -isTracked (Iso.inv (PERMorphism≡Iso {R} {S} f g) fMap≡gMap i) = - isProp→PathP - (λ i → - isPropPropTrunc - {A = Σ[ e ∈ A ] (∀ (a : A) → ∣ R ∣ a a → ((fMap≡gMap i) [ a ] ≡ [ e ⨾ a ]) × ∣ S ∣ (e ⨾ a) (e ⨾ a))}) - (f .isTracked) (g .isTracked) i -Iso.rightInv (PERMorphism≡Iso {R} {S} f g) fMap≡gMap = refl -Iso.leftInv (PERMorphism≡Iso {R} {S} f g) f≡g = isSetPERMorphism f g (Iso.inv (PERMorphism≡Iso f g) (λ i → f≡g i .map)) f≡g - -PERMorphism≡ : ∀ {R S} → (f g : PERMorphism R S) → f .map ≡ g .map → f ≡ g -PERMorphism≡ {R} {S} f g fMap≡gMap = Iso.inv (PERMorphism≡Iso f g) fMap≡gMap - -idPERMorphism : ∀ {R : PER} → PERMorphism R R -map (idPERMorphism {R}) x = x -isTracked (idPERMorphism {R}) = - return (Id , (λ a aRa → (subst (λ r → [ a ] ≡ [ r ]) (sym (Ida≡a a)) refl) , (subst (λ r → ∣ R ∣ r r) (sym (Ida≡a a)) aRa))) - -composePERMorphism : ∀ {R S T : PER} → PERMorphism R S → PERMorphism S T → PERMorphism R T -map (composePERMorphism {R} {S} {T} f g) x = g .map (f .map x) -isTracked (composePERMorphism {R} {S} {T} f g) = - do - (f~ , isTrackedF) ← f .isTracked - (g~ , isTrackedG) ← g .isTracked - let - realizer : Term as 1 - realizer = ` g~ ̇ (` f~ ̇ # zero) - return - (λ* realizer , - (λ a aRa → - (g .map (f .map [ a ]) - ≡⟨ cong (g .map) (isTrackedF a aRa .fst) ⟩ - g .map [ f~ ⨾ a ] - ≡⟨ isTrackedG (f~ ⨾ a) (isTrackedF a aRa .snd) .fst ⟩ - [ g~ ⨾ (f~ ⨾ a) ] - ≡⟨ cong [_] (sym (λ*ComputationRule realizer a)) ⟩ - [ λ* realizer ⨾ a ] - ∎) , - (subst (λ r' → ∣ T ∣ r' r') (sym (λ*ComputationRule realizer a)) (isTrackedG (f~ ⨾ a) (isTrackedF a aRa .snd) .snd)))) - --- all definitional -idLPERMorphism : ∀ {R S} → (f : PERMorphism R S) → composePERMorphism idPERMorphism f ≡ f -idLPERMorphism {R} {S} f = PERMorphism≡ _ _ refl - -idRPERMorphism : ∀ {R S} → (f : PERMorphism R S) → composePERMorphism f idPERMorphism ≡ f -idRPERMorphism {R} {S} f = PERMorphism≡ _ _ refl - -assocPERMorphism : - ∀ {R S T U} - → (f : PERMorphism R S) - → (g : PERMorphism S T) - → (h : PERMorphism T U) - → composePERMorphism (composePERMorphism f g) h ≡ composePERMorphism f (composePERMorphism g h) -assocPERMorphism {R} {S} {T} {U} f g h = PERMorphism≡ _ _ refl +_~[_]_ : A → PER → A → Type ℓ +a ~[ R ] b = R .relation .fst a b + +isProp~ : ∀ a R b → isProp (a ~[ R ] b) +isProp~ a R b = R .relation .snd a b + +isTracker : (R S : PER) → A → Type ℓ +isTracker R S a = ∀ r r' → r ~[ R ] r' → (a ⨾ r) ~[ S ] (a ⨾ r') + +perTracker : (R S : PER) → Type ℓ +perTracker R S = Σ[ a ∈ A ] isTracker R S a + +isEquivTracker : (R S : PER) → perTracker R S → perTracker R S → Type ℓ +isEquivTracker R S (a , _) (b , _) = (∀ r → r ~[ R ] r → (a ⨾ r) ~[ S ] (b ⨾ r)) + +isEquivRelIsEquivTracker : (R S : PER) → BR.isEquivRel (isEquivTracker R S) +BinaryRelation.isEquivRel.reflexive (isEquivRelIsEquivTracker R S) (a , isTrackerA) r r~r = isTrackerA r r r~r +BinaryRelation.isEquivRel.symmetric (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) a~b r r~r = isSymmetric S (a ⨾ r) (b ⨾ r) (a~b r r~r) +BinaryRelation.isEquivRel.transitive (isEquivRelIsEquivTracker R S) (a , isTrackerA) (b , isTrackerB) (c , isTrackerC) a~b b~c r r~r = isTransitive S (a ⨾ r) (b ⨾ r) (c ⨾ r) (a~b r r~r) (b~c r r~r) + +isPropIsEquivTracker : ∀ R S a b → isProp (isEquivTracker R S a b) +isPropIsEquivTracker R S (a , isTrackerA) (b , isTrackerB) = isPropΠ2 λ r r~r → isPropValued S (a ⨾ r) (b ⨾ r) + +isEffectiveIsEquivTracker : ∀ R S → BR.isEffective (isEquivTracker R S) +isEffectiveIsEquivTracker R S = isEquivRel→isEffective (isPropIsEquivTracker R S) (isEquivRelIsEquivTracker R S) + +perMorphism : (R S : PER) → Type ℓ +perMorphism R S = perTracker R S / (isEquivTracker R S) + +effectiveIsEquivTracker : ∀ R S a b → [ a ] ≡ [ b ] → isEquivTracker R S a b +effectiveIsEquivTracker R S a b eq' = effective (isPropIsEquivTracker R S) (isEquivRelIsEquivTracker R S) a b eq' + +isSetPerMorphism : ∀ R S → isSet (perMorphism R S) +isSetPerMorphism R S = squash/ + +idPerMorphism : (R : PER) → perMorphism R R +idPerMorphism R = [ Id , (λ r r' r~r' → subst2 (λ r r' → r ~[ R ] r') (sym (Ida≡a r)) (sym (Ida≡a r')) r~r') ] + +composePerTracker : (R S T : PER) → perTracker R S → perTracker S T → perTracker R T +composePerTracker R S T (a , a⊩f) (b , b⊩g) = + let + realizer : Term as 1 + realizer = ` b ̇ (` a ̇ # zero) + in + λ* realizer , + λ r r' r~r' → + subst2 + _~[ T ]_ + (sym (λ*ComputationRule realizer r)) + (sym (λ*ComputationRule realizer r')) + (b⊩g (a ⨾ r) (a ⨾ r') (a⊩f r r' r~r')) + +composePerMorphism : (R S T : PER) → perMorphism R S → perMorphism S T → perMorphism R T +composePerMorphism R S T f g = + SQ.rec2 + squash/ + (λ { (a , a⊩f) (b , b⊩g) → + [ composePerTracker R S T (a , a⊩f) (b , b⊩g) ] }) + (λ { (a , a⊩f) (b , b⊩f) (c , c⊩g) a~b → + eq/ _ _ + λ r r~r → + subst2 + (λ car cbr → car ~[ T ] cbr) + (sym (λ*ComputationRule (` c ̇ (` a ̇ # zero)) r)) + (sym (λ*ComputationRule (` c ̇ (` b ̇ # zero)) r)) + (c⊩g (a ⨾ r) (b ⨾ r) (a~b r r~r)) }) + (λ { (a , a⊩f) (b , b⊩g) (c , c⊩g) b~c → + eq/ _ _ + λ r r~r → + subst2 + (λ bar car → bar ~[ T ] car) + (sym (λ*ComputationRule (` b ̇ (` a ̇ # zero)) r)) + (sym (λ*ComputationRule (` c ̇ (` a ̇ # zero)) r)) + (b~c (a ⨾ r) (a⊩f r r r~r)) }) + f g + +idLPerMorphism : ∀ R S f → composePerMorphism R R S (idPerMorphism R) f ≡ f +idLPerMorphism R S f = + SQ.elimProp + (λ f → squash/ (composePerMorphism R R S (idPerMorphism R) f) f) + (λ { (a , a⊩f) → + eq/ _ _ + λ r r~r → + subst + (λ ar → ar ~[ S ] (a ⨾ r)) + (sym (λ*ComputationRule (` a ̇ (` Id ̇ # zero)) r ∙ cong (λ x → a ⨾ x) (Ida≡a r))) + (a⊩f r r r~r) }) + f + +idRPerMorphism : ∀ R S f → composePerMorphism R S S f (idPerMorphism S) ≡ f +idRPerMorphism R S f = + SQ.elimProp + (λ f → squash/ (composePerMorphism R S S f (idPerMorphism S)) f) + (λ { (a , a⊩f) → + eq/ _ _ + λ r r~r → + subst (λ ar → ar ~[ S ] (a ⨾ r)) (sym (λ*ComputationRule (` Id ̇ (` a ̇ # zero)) r ∙ Ida≡a (a ⨾ r))) (a⊩f r r r~r) }) + f + +assocPerMorphism : ∀ R S T U f g h → composePerMorphism R T U (composePerMorphism R S T f g) h ≡ composePerMorphism R S U f (composePerMorphism S T U g h) +assocPerMorphism R S T U f g h = + SQ.elimProp3 + (λ f g h → squash/ (composePerMorphism R T U (composePerMorphism R S T f g) h) (composePerMorphism R S U f (composePerMorphism S T U g h))) + (λ { (a , a⊩f) (b , b⊩g) (c , c⊩h) → + eq/ _ _ + λ r r~r → + subst2 + (λ cba cba' → cba ~[ U ] cba') + (sym (λ*ComputationRule (` c ̇ (` ⟦ as ⟧ (λ*abst (` b ̇ (` a ̇ # zero))) [] ̇ # zero)) r ∙ cong (λ bar → c ⨾ bar) (λ*ComputationRule (` b ̇ (` a ̇ # zero)) r))) + (sym (λ*ComputationRule (` ⟦ as ⟧ (λ*abst (` c ̇ (` b ̇ # zero))) [] ̇ (` a ̇ # zero)) r ∙ λ*ComputationRule (` c ̇ (` b ̇ # zero)) (a ⨾ r))) + (c⊩h (b ⨾ (a ⨾ r)) (b ⨾ (a ⨾ r)) (b⊩g (a ⨾ r) (a ⨾ r) (a⊩f r r r~r)) ) }) + f g h PERCat : Category (ℓ-suc ℓ) ℓ Category.ob PERCat = PER -Category.Hom[_,_] PERCat R S = PERMorphism R S -Category.id PERCat {R} = idPERMorphism -Category._⋆_ PERCat {R} {S} {T} f g = composePERMorphism f g -Category.⋆IdL PERCat f = idLPERMorphism f -Category.⋆IdR PERCat f = idRPERMorphism f -Category.⋆Assoc PERCat f g h = assocPERMorphism f g h -Category.isSetHom PERCat = isSetPERMorphism - -open Assembly - -inclusion : Functor PERCat ASM -fst (Functor.F-ob inclusion per) = Σ[ a ∈ A ] ∣ per ∣ a a -(snd (Functor.F-ob inclusion per)) ._⊩_ r (a , aRa) = ∣ per ∣ r a -isSetX (snd (Functor.F-ob inclusion per)) = isSetΣ isSetA (λ x → isProp→isSet (isPropValued per x x)) -⊩isPropValued (snd (Functor.F-ob inclusion per)) r (a , aRa) = isPropValued per r a -⊩surjective (snd (Functor.F-ob inclusion per)) (a , aRa) = return (a , aRa) -AssemblyMorphism.map (Functor.F-hom inclusion morphism) (a , aRa) = {!!} -AssemblyMorphism.tracker (Functor.F-hom inclusion morphism) = {!!} -Functor.F-id inclusion = {!!} -Functor.F-seq inclusion = {!!} +Category.Hom[_,_] PERCat R S = perMorphism R S +Category.id PERCat {R} = idPerMorphism R +Category._⋆_ PERCat {R} {S} {T} f g = composePerMorphism R S T f g +Category.⋆IdL PERCat {R} {S} f = idLPerMorphism R S f +Category.⋆IdR PERCat {R} {S} f = idRPerMorphism R S f +Category.⋆Assoc PERCat {R} {S} {T} {U} f g h = assocPerMorphism R S T U f g h +Category.isSetHom PERCat {R} {S} = isSetPerMorphism R S diff --git a/src/Realizability/PERs/TerminalObject.agda b/src/Realizability/PERs/TerminalObject.agda index c3a6576..5f2bd62 100644 --- a/src/Realizability/PERs/TerminalObject.agda +++ b/src/Realizability/PERs/TerminalObject.agda @@ -26,7 +26,6 @@ module Realizability.PERs.TerminalObject open import Realizability.PERs.PER ca open CombinatoryAlgebra ca open Combinators ca renaming (i to Id; ia≡a to Ida≡a) -open PERMorphism terminalPER : PER PER.relation terminalPER = (λ x y → Unit*) , λ x y → isPropUnit* @@ -36,8 +35,13 @@ snd (PER.isPER terminalPER) = λ a b c x x₁ → tt* isTerminalTerminalPER : isTerminal PERCat terminalPER isTerminalTerminalPER X = inhProp→isContr - (makePERMorphism (λ x → [ k ]) (return (Id , (λ a aXa → (eq/ k (Id ⨾ a) tt*) , tt*)))) - λ x y → PERMorphism≡ x y (funExt λ q → {!!}) + [ k , (λ r r' r~r' → tt*) ] + λ ! !' → + SQ.elimProp2 + (λ ! !' → squash/ ! !') + (λ { (a , a⊩!) (b , b⊩!) → + eq/ _ _ λ r r~r → tt* }) + ! !' terminal : Terminal PERCat -terminal = terminalPER , {!!} +terminal = terminalPER , isTerminalTerminalPER diff --git a/src/Utils/SQElim.agda b/src/Utils/SQElim.agda new file mode 100644 index 0000000..d138409 --- /dev/null +++ b/src/Utils/SQElim.agda @@ -0,0 +1,52 @@ +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Path +open import Cubical.HITs.SetQuotients as SQ + +module Utils.SQElim where + +private + variable + ℓ ℓ' ℓ'' : Level + A B C Q : Type ℓ + R S T W : A → A → Type ℓ + +elim2 : {P : A / R → B / S → Type ℓ} + → (∀ x y → isSet (P x y)) + → (f : ∀ a b → P [ a ] [ b ]) + → (∀ a b c → (s : S b c) → PathP (λ i → P [ a ] (eq/ b c s i)) (f a b) (f a c)) + → (∀ a b c → (r : R a b) → PathP (λ i → P (eq/ a b r i) [ c ]) (f a c) (f b c)) + → ∀ x y → P x y +elim2 {P = P} isSetP f coh1 coh2 x y = + SQ.elim + {P = λ x → ∀ y → P x y} + (λ x → isSetΠ λ y → isSetP x y) + (λ a y → + SQ.elim + {P = λ y → P [ a ] y} + (λ y → isSetP [ a ] y) + (λ b → f a b) + (λ b c r → coh1 a b c r) + y) + (λ a b r → + funExt + λ z → + SQ.elimProp + {P = λ z → PathP (λ z₁ → P (eq/ a b r z₁) z) (elim (λ y₁ → isSetP [ a ] y₁) (λ b₁ → f a b₁) (λ b₁ c r₁ → coh1 a b₁ c r₁) z) (elim (λ y₁ → isSetP [ b ] y₁) (λ b₁ → f b b₁) (λ b₁ c r₁ → coh1 b b₁ c r₁) z)} + (λ z p q i j → + isSet→SquareP + {A = λ i' j' → P (eq/ a b r j') z} + (λ i' j' → isSetP (eq/ a b r j') z) + {a₀₀ = elim (isSetP [ a ]) (f a) (coh1 a) z} + {a₀₁ = elim (isSetP [ b ]) (f b) (coh1 b) z} + p + {a₁₀ = elim (isSetP [ a ]) (f a) (coh1 a) z} + {a₁₁ = elim (isSetP [ b ]) (f b) (coh1 b) z} + q + refl + refl + i j) + (λ c → coh2 a b c r) + z) + x y +