Skip to content

Commit

Permalink
Define Small PERs and Equivalence to ordinary PERs
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahulc29
rahulc29 committed Jun 27, 2024
1 parent 73d04b5 commit 1c1ecc3
Show file tree
Hide file tree
Showing 2 changed files with 147 additions and 26 deletions.
64 changes: 55 additions & 9 deletions src/Realizability/PERs/PER.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand All @@ -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')
Expand Down
109 changes: 92 additions & 17 deletions src/Realizability/PERs/ResizedPER.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand All @@ -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))
Expand All @@ -62,30 +68,99 @@ 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
field
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

0 comments on commit 1c1ecc3

Please sign in to comment.