From 1c1ecc390e7ce0f4b1135e7b2e3cd6d8597c8b45 Mon Sep 17 00:00:00 2001 From: Rahul Chhabra Date: Thu, 27 Jun 2024 20:26:42 +0530 Subject: [PATCH] Define Small PERs and Equivalence to ordinary PERs --- src/Realizability/PERs/PER.agda | 64 +++++++++++++-- src/Realizability/PERs/ResizedPER.agda | 109 +++++++++++++++++++++---- 2 files changed, 147 insertions(+), 26 deletions(-) diff --git a/src/Realizability/PERs/PER.agda b/src/Realizability/PERs/PER.agda index 236b9b4..923f455 100644 --- a/src/Realizability/PERs/PER.agda +++ b/src/Realizability/PERs/PER.agda @@ -30,11 +30,11 @@ open Combinators ca renaming (i to Id; ia≡a to Ida≡a) module BR = BinaryRelation -isPartialEquivalenceRelation : PropRel A A ℓ → Type _ -isPartialEquivalenceRelation (rel , isPropValuedRel) = BR.isSym rel × BR.isTrans rel +isPartialEquivalenceRelation : (A → A → Type ℓ) → Type _ +isPartialEquivalenceRelation rel = BR.isSym rel × BR.isTrans rel -isPropIsPartialEquivalenceRelation : ∀ r → isProp (isPartialEquivalenceRelation r) -isPropIsPartialEquivalenceRelation (rel , isPropValuedRel) = +isPropIsPartialEquivalenceRelation : ∀ r → (∀ a b → isProp (r a b)) → isProp (isPartialEquivalenceRelation r) +isPropIsPartialEquivalenceRelation rel isPropValuedRel = isProp× (isPropΠ (λ x → isPropΠ λ y → isProp→ (isPropValuedRel y x))) (isPropΠ λ x → isPropΠ λ y → isPropΠ λ z → isProp→ (isProp→ (isPropValuedRel x z))) @@ -43,20 +43,66 @@ record PER : Type (ℓ-suc ℓ) where no-eta-equality constructor makePER field - relation : PropRel A A ℓ + relation : A → A → Type ℓ + isPropValued : ∀ a b → isProp (relation a b) isPER : isPartialEquivalenceRelation relation - ∣_∣ = relation .fst isSymmetric = isPER .fst isTransitive = isPER .snd - isPropValued = relation .snd open PER +PERΣ : Type (ℓ-suc ℓ) +PERΣ = Σ[ relation ∈ (A → A → hProp ℓ) ] isPartialEquivalenceRelation λ a b → ⟨ relation a b ⟩ + +isSetPERΣ : isSet PERΣ +isSetPERΣ = + isSetΣ + (isSet→ (isSet→ isSetHProp)) + (λ relation → + isProp→isSet + (isPropIsPartialEquivalenceRelation + (λ a b → ⟨ relation a b ⟩) + (λ a b → str (relation a b)))) + +PER≡ : ∀ (R S : PER) → (R .relation ≡ S .relation) → R ≡ S +relation (PER≡ R S rel≡ i) = rel≡ i +isPropValued (PER≡ R S rel≡ i) a b = + isProp→PathP + {B = λ j → isProp (rel≡ j a b)} + (λ j → isPropIsProp) + (R .isPropValued a b) + (S .isPropValued a b) i +isPER (PER≡ R S rel≡ i) = + isProp→PathP + {B = λ j → isPartialEquivalenceRelation (rel≡ j)} + (λ j → isPropIsPartialEquivalenceRelation (rel≡ j) λ a b → isPropRelJ a b j) + (R .isPER) + (S .isPER) i where + isPropRelJ : ∀ a b j → isProp (rel≡ j a b) + isPropRelJ a b j = isProp→PathP {B = λ k → isProp (rel≡ k a b)} (λ k → isPropIsProp) (R .isPropValued a b) (S .isPropValued a b) j + +PERIsoΣ : Iso PER PERΣ +Iso.fun PERIsoΣ per = (λ a b → per .relation a b , per .isPropValued a b) , per .isPER +relation (Iso.inv PERIsoΣ perΣ) a b = ⟨ perΣ .fst a b ⟩ +isPropValued (Iso.inv PERIsoΣ perΣ) a b = str (perΣ .fst a b) +isPER (Iso.inv PERIsoΣ perΣ) = perΣ .snd +Iso.rightInv PERIsoΣ perΣ = refl +Iso.leftInv PERIsoΣ per = PER≡ _ _ refl + +isSetPER : isSet PER +isSetPER = isOfHLevelRetractFromIso 2 PERIsoΣ isSetPERΣ + +PER≡Iso : ∀ (R S : PER) → Iso (R ≡ S) (R .relation ≡ S .relation) +Iso.fun (PER≡Iso R S) R≡S i = R≡S i .relation +Iso.inv (PER≡Iso R S) rel≡ = PER≡ R S rel≡ +Iso.rightInv (PER≡Iso R S) rel≡ = refl +Iso.leftInv (PER≡Iso R S) R≡S = isSetPER R S _ _ + _~[_]_ : A → PER → A → Type ℓ -a ~[ R ] b = R .relation .fst a b +a ~[ R ] b = R .relation a b isProp~ : ∀ a R b → isProp (a ~[ R ] b) -isProp~ a R b = R .relation .snd a b +isProp~ a R b = R .isPropValued a b isTracker : (R S : PER) → A → Type ℓ isTracker R S a = ∀ r r' → r ~[ R ] r' → (a ⨾ r) ~[ S ] (a ⨾ r') diff --git a/src/Realizability/PERs/ResizedPER.agda b/src/Realizability/PERs/ResizedPER.agda index 4575301..c8b5b16 100644 --- a/src/Realizability/PERs/ResizedPER.agda +++ b/src/Realizability/PERs/ResizedPER.agda @@ -8,7 +8,7 @@ open import Cubical.Foundations.Equiv open import Cubical.Foundations.Univalence open import Cubical.Foundations.Powerset open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.Path open import Cubical.Functions.FunExtEquiv open import Cubical.Relation.Binary open import Cubical.Data.Sigma @@ -35,6 +35,9 @@ smallHProp = resizing .fst hProp≃smallHProp = resizing .snd smallHProp≃hProp = invEquiv hProp≃smallHProp +isSetSmallHProp : isSet smallHProp +isSetSmallHProp = isOfHLevelRespectEquiv 2 hProp≃smallHProp isSetHProp + hPropIsoSmallHProp : Iso (hProp ℓ) smallHProp hPropIsoSmallHProp = equivToIso hProp≃smallHProp @@ -53,6 +56,9 @@ shrink⋆enlarge≡id = Iso.leftInv hPropIsoSmallHProp extractType : smallHProp → Type ℓ extractType p = ⟨ enlarge p ⟩ +isPropExtractType : ∀ p → isProp (extractType p) +isPropExtractType p = str (enlarge p) + extractFromShrunk : ∀ p isPropP → extractType (shrink (p , isPropP)) ≡ p extractFromShrunk p isPropP = extractType (shrink (p , isPropP)) @@ -62,6 +68,15 @@ extractFromShrunk p isPropP = p ∎ +shrinkFromExtracted : ∀ p → shrink (extractType p , isPropExtractType p) ≡ p +shrinkFromExtracted p = + shrink (extractType p , isPropExtractType p) + ≡⟨ refl ⟩ + shrink (enlarge p) + ≡⟨ enlarge⋆shrink≡id p ⟩ + p + ∎ + record ResizedPER : Type ℓ where no-eta-equality constructor makeResizedPER @@ -69,23 +84,83 @@ record ResizedPER : Type ℓ where relation : A → A → smallHProp isSymmetric : ∀ a b → extractType (relation a b) → extractType (relation b a) isTransitive : ∀ a b c → extractType (relation a b) → extractType (relation b c) → extractType (relation a c) - + open ResizedPER -ResizedPERHAEquivPER : HAEquiv ResizedPER PER -PER.relation (fst ResizedPERHAEquivPER resized) = - (λ a b → extractType (resized .relation a b)) , - λ a b → str (enlarge (resized .relation a b)) -fst (PER.isPER (fst ResizedPERHAEquivPER resized)) a b a~b = resized .isSymmetric a b a~b -snd (PER.isPER (fst ResizedPERHAEquivPER resized)) a b c a~b b~c = resized .isTransitive a b c a~b b~c -relation (isHAEquiv.g (snd ResizedPERHAEquivPER) per) a b = - shrink ((per .PER.relation .fst a b) , (per .PER.relation .snd a b)) -isSymmetric (isHAEquiv.g (snd ResizedPERHAEquivPER) per) a b a~b = - subst _ (sym (extractFromShrunk (per .PER.relation .fst b a) (per .PER.relation .snd b a))) {!per .PER.isPER .fst a b a~b!} -isTransitive (isHAEquiv.g (snd ResizedPERHAEquivPER) per) a b c a~b b~c = {!!} -isHAEquiv.linv (snd ResizedPERHAEquivPER) resized = {!!} -isHAEquiv.rinv (snd ResizedPERHAEquivPER) per = {!!} -isHAEquiv.com (snd ResizedPERHAEquivPER) resized = {!!} +unquoteDecl ResizedPERIsoΣ = declareRecordIsoΣ ResizedPERIsoΣ (quote ResizedPER) + +ResizedPERΣ : Type ℓ +ResizedPERΣ = + Σ[ relation ∈ (A → A → smallHProp) ] + (∀ a b → extractType (relation a b) → extractType (relation b a)) × + (∀ a b c → extractType (relation a b) → extractType (relation b c) → extractType (relation a c)) + +isSetResizedPERΣ : isSet ResizedPERΣ +isSetResizedPERΣ = + isSetΣ + (isSet→ (isSet→ isSetSmallHProp)) + (λ relation → isProp→isSet (isProp× (isPropΠ3 λ _ _ _ → isPropExtractType _) (isPropΠ5 λ _ _ _ _ _ → isPropExtractType _))) + +isSetResizedPER : isSet ResizedPER +isSetResizedPER = isOfHLevelRetractFromIso 2 ResizedPERIsoΣ isSetResizedPERΣ + +ResizedPER≡Iso : ∀ (R S : ResizedPER) → Iso (R ≡ S) (∀ a b → R .relation a b ≡ S .relation a b) +Iso.fun (ResizedPER≡Iso R S) R≡S a b i = (R≡S i) .relation a b +relation (Iso.inv (ResizedPER≡Iso R S) pointwise i) a b = pointwise a b i +isSymmetric (Iso.inv (ResizedPER≡Iso R S) pointwise i) = + isProp→PathP + {B = λ j → (a b : A) → extractType (pointwise a b j) → extractType (pointwise b a j)} + (λ j → isPropΠ3 λ _ _ _ → isPropExtractType _) + (isSymmetric R) + (isSymmetric S) i +isTransitive (Iso.inv (ResizedPER≡Iso R S) pointwise i) = + isProp→PathP + {B = λ j → (a b c : A) → extractType (pointwise a b j) → extractType (pointwise b c j) → extractType (pointwise a c j)} + (λ j → isPropΠ5 λ _ _ _ _ _ → isPropExtractType _) + (R .isTransitive) + (S .isTransitive) + i +Iso.rightInv (ResizedPER≡Iso R S) pointwise = refl +Iso.leftInv (ResizedPER≡Iso R S) R≡S = isSetResizedPER R S _ _ + +ResizedPER≡ : ∀ (R S : ResizedPER) → (∀ a b → R .relation a b ≡ S .relation a b) → R ≡ S +ResizedPER≡ R S pointwise = Iso.inv (ResizedPER≡Iso R S) pointwise + +ResizedPERIsoPER : Iso ResizedPER PER +PER.relation (Iso.fun ResizedPERIsoPER resized) a b = extractType (resized .relation a b) +PER.isPropValued (Iso.fun ResizedPERIsoPER resized) a b = isPropExtractType _ +fst (PER.isPER (Iso.fun ResizedPERIsoPER resized)) a b a~b = resized .isSymmetric a b a~b +snd (PER.isPER (Iso.fun ResizedPERIsoPER resized)) a b c a~b b~c = resized .isTransitive a b c a~b b~c +relation (Iso.inv ResizedPERIsoPER per) a b = shrink (per .PER.relation a b , per .PER.isPropValued a b) +isSymmetric (Iso.inv ResizedPERIsoPER per) a b a~[resized]b = b~[resized]a where + a~b : per .PER.relation a b + a~b = transport (extractFromShrunk _ _) a~[resized]b + + b~a : per .PER.relation b a + b~a = per .PER.isPER .fst a b a~b + + b~[resized]a : extractType (shrink (per .PER.relation b a , per .PER.isPropValued b a)) + b~[resized]a = transport (sym (extractFromShrunk _ _)) b~a +isTransitive (Iso.inv ResizedPERIsoPER per) a b c a~[resized]b b~[resized]c = a~[resized]c where + a~b : per .PER.relation a b + a~b = transport (extractFromShrunk _ _) a~[resized]b + + b~c : per .PER.relation b c + b~c = transport (extractFromShrunk _ _) b~[resized]c + + a~c : per .PER.relation a c + a~c = per .PER.isPER .snd a b c a~b b~c + + a~[resized]c : extractType (shrink (per .PER.relation a c , per .PER.isPropValued a c)) + a~[resized]c = transport (sym (extractFromShrunk _ _)) a~c +Iso.rightInv ResizedPERIsoPER per = + PER≡ _ _ + (funExt₂ + λ a b → + extractFromShrunk (per .PER.relation a b) (per .PER.isPropValued a b)) +Iso.leftInv ResizedPERIsoPER resizedPer = + ResizedPER≡ _ _ + λ a b → shrinkFromExtracted (resizedPer .relation a b) ResizedPER≃PER : ResizedPER ≃ PER -ResizedPER≃PER = ResizedPERHAEquivPER .fst , isHAEquiv→isEquiv (ResizedPERHAEquivPER .snd) +ResizedPER≃PER = isoToEquiv ResizedPERIsoPER