Skip to content

Commit cd94b8c

Browse files
anshwad10anshwad10
authored
Intervals in posets and the covering relation (#1219)
* Add files via upload * Delete Base.agda No idea what this file is doing here * Delete Properties.agda Must have accidentally put this here when I was editing dagger-cat * Define the category of posets * Use IsIsotone from Poset.Mappings I also added a constructor of IsIsotone like IsAntitone * Define the (downward/upward) closure of a subset * add ∃-rec and ∃-elim, lemmas about downward/upward closure * Simplify the membership lemmas using fiberEquiv * The universal property of the downward closure * fix spacing and naming * Define the interval between two elements, define Iso→Embedding * Define the covering relation * The set of faces and cofaces * private variable declaration * Delete Graded.agda I'll define that later * fix whitespace
1 parent 294e796 commit cd94b8c

File tree

3 files changed

+156
-0
lines changed

3 files changed

+156
-0
lines changed

‎Cubical/Functions/Embedding.agda‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,10 @@ iso→isEmbedding : ∀ {ℓ} {A B : Type ℓ}
190190
→ isEmbedding (Iso.fun isom)
191191
iso→isEmbedding {A = A} {B} isom = (isEquiv→isEmbedding (equivIsEquiv (isoToEquiv isom)))
192192

193+
Iso→Embedding : ∀ {ℓ} {A B : Type ℓ}
194+
→ Iso A B → A ↪ B
195+
Iso→Embedding isom = _ , iso→isEmbedding isom
196+
193197
isEmbedding→Injection :
194198
∀ {ℓ} {A B C : Type ℓ}
195199
→ (a : A → B)

‎Cubical/Relation/Binary/Order/Poset/Covering.agda‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
-- The covering relation
2+
{-# OPTIONS --safe #-}
3+
4+
module Cubical.Relation.Binary.Order.Poset.Covering where
5+
6+
open import Cubical.Foundations.Equiv
7+
open import Cubical.Foundations.HLevels
8+
open import Cubical.Foundations.Isomorphism
9+
open import Cubical.Foundations.Prelude
10+
open import Cubical.Foundations.Function
11+
open import Cubical.Foundations.Structure
12+
open import Cubical.Foundations.Transport
13+
14+
open import Cubical.Functions.Embedding
15+
open import Cubical.Functions.Fibration
16+
17+
open import Cubical.Data.Bool as B using (Bool; true; false)
18+
open import Cubical.Data.Sum as ⊎
19+
open import Cubical.Data.Empty as ⊥
20+
21+
open import Cubical.Relation.Binary.Order.Poset.Base
22+
open import Cubical.Relation.Binary.Order.Poset.Properties
23+
open import Cubical.Relation.Binary.Order.Poset.Subset
24+
open import Cubical.Relation.Binary.Order.Poset.Interval
25+
open import Cubical.Relation.Nullary
26+
27+
open import Cubical.Reflection.RecordEquiv
28+
29+
private variable
30+
ℓ ℓ' : Level
31+
32+
module Cover (P' : Poset ℓ ℓ') where
33+
private P = ⟨ P' ⟩
34+
open PosetStr (snd P')
35+
36+
infixl 20 _covers_
37+
38+
_covers_ : P → P → Type (ℓ-max ℓ ℓ')
39+
y covers x = Σ[ x≤y ∈ x ≤ y ] isEquiv (2→Interval P' x y x≤y)
40+
41+
isPropCovers : ∀ y x → isProp (y covers x)
42+
isPropCovers y x = isPropΣ (is-prop-valued x y) (λ _ → isPropIsEquiv _)
43+
44+
module _ (x y : P) (x≤y : x ≤ y) (x≠y : ¬ x ≡ y)
45+
(cov : ∀ z → x ≤ z → z ≤ y → (z ≡ x) ⊎ (z ≡ y)) where
46+
open Iso
47+
48+
private
49+
cov' : (i : Interval P' x y) → (i .Interval.z ≡ x) ⊎ (i .Interval.z ≡ y)
50+
cov' (interval z x≤z z≤y) = cov z x≤z z≤y
51+
52+
makeCovers : y covers x
53+
makeCovers = x≤y , isoToIsEquiv isom where
54+
55+
isom : Iso Bool (Interval P' x y)
56+
isom .fun = 2→Interval P' x y x≤y
57+
isom .inv i with cov' i
58+
... | inl z≡x = false
59+
... | inr z≡y = true
60+
isom .rightInv i with cov' i
61+
... | inl z≡x = Interval≡ P' x y _ _ (sym z≡x)
62+
... | inr z≡y = Interval≡ P' x y _ _ (sym z≡y)
63+
isom .leftInv b with cov' (2→Interval P' x y x≤y b)
64+
isom .leftInv false | inl _ = refl
65+
isom .leftInv false | inr x≡y = ⊥.rec (x≠y x≡y)
66+
isom .leftInv true | inl y≡x = ⊥.rec (x≠y (sym y≡x))
67+
isom .leftInv true | inr _ = refl
68+
69+
-- Subset of faces and cofaces
70+
-- terminology from "Combinatorics of higher-categorical diagrams" by Amar Hadzihasanovic
71+
Δ : P → Embedding P (ℓ-max ℓ ℓ')
72+
Δ x = (Σ[ y ∈ P ] x covers y) , EmbeddingΣProp λ _ → isPropCovers _ _
73+
74+
∇ : P → Embedding P (ℓ-max ℓ ℓ')
75+
∇ x = (Σ[ y ∈ P ] y covers x) , EmbeddingΣProp λ _ → isPropCovers _ _
76+
77+
ΔMembership : ∀ x y → x covers y ≃ y ∈ₑ Δ x
78+
ΔMembership x y = invEquiv (fiberEquiv _ _)
79+
80+
∇Membership : ∀ x y → y covers x ≃ y ∈ₑ ∇ x
81+
∇Membership x y = invEquiv (fiberEquiv _ _)

‎Cubical/Relation/Binary/Order/Poset/Interval.agda‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
{-# OPTIONS --safe #-}
2+
3+
module Cubical.Relation.Binary.Order.Poset.Interval where
4+
5+
open import Cubical.Foundations.Equiv
6+
open import Cubical.Foundations.HLevels
7+
open import Cubical.Foundations.Prelude
8+
open import Cubical.Foundations.Function
9+
open import Cubical.Foundations.Structure
10+
open import Cubical.Foundations.Transport
11+
open import Cubical.Foundations.Isomorphism
12+
13+
open import Cubical.Functions.Embedding
14+
open import Cubical.Functions.Fibration
15+
16+
open import Cubical.Data.Bool as B using (Bool; true; false)
17+
open import Cubical.Data.Sigma
18+
19+
open import Cubical.Relation.Binary.Order.Poset.Base
20+
open import Cubical.Relation.Binary.Order.Poset.Properties
21+
open import Cubical.Relation.Binary.Order.Poset.Subset
22+
23+
open import Cubical.Reflection.RecordEquiv
24+
25+
private variable
26+
ℓ ℓ' : Level
27+
28+
module _ (P' : Poset ℓ ℓ') where
29+
private P = ⟨ P' ⟩
30+
open PosetStr (snd P')
31+
32+
module _ (x y : P) where
33+
-- the set of elements between x and y
34+
record Interval : Type (ℓ-max ℓ ℓ') where
35+
constructor interval
36+
field
37+
z : P
38+
x≤z : x ≤ z
39+
z≤y : z ≤ y
40+
41+
unquoteDecl IntervalIsoΣ = declareRecordIsoΣ IntervalIsoΣ (quote Interval)
42+
43+
isSetInterval : isSet Interval
44+
isSetInterval = isOfHLevelRetractFromIso 2 IntervalIsoΣ $
45+
isSetΣSndProp is-set λ _ → isProp× (is-prop-valued _ _) (is-prop-valued _ _)
46+
47+
Interval↪ : Interval ↪ P
48+
Interval↪ = compEmbedding (EmbeddingΣProp λ _ → isProp× (is-prop-valued _ _) (is-prop-valued _ _)) (Iso→Embedding IntervalIsoΣ)
49+
50+
IntervalEmbedding : Embedding P (ℓ-max ℓ ℓ')
51+
IntervalEmbedding = Interval , Interval↪
52+
53+
IntervalPosetStr : PosetStr ℓ' Interval
54+
IntervalPosetStr = posetstr _ (isPosetInduced isPoset Interval Interval↪)
55+
56+
IntervalPoset : Poset (ℓ-max ℓ ℓ') ℓ'
57+
IntervalPoset = Interval , IntervalPosetStr
58+
59+
Interval≡ : ∀ i j → i .Interval.z ≡ j .Interval.z → i ≡ j
60+
Interval≡ _ _ = isoFunInjective IntervalIsoΣ _ _ ∘ Σ≡Prop (λ _ → isProp× (is-prop-valued _ _) (is-prop-valued _ _))
61+
62+
module _ (x≤y : x ≤ y) where
63+
intervalTop : Interval
64+
intervalTop = interval y x≤y (is-refl y)
65+
66+
intervalBot : Interval
67+
intervalBot = interval x (is-refl x) x≤y
68+
69+
2→Interval : Bool → Interval
70+
2→Interval false = intervalBot
71+
2→Interval true = intervalTop

0 commit comments

Comments
 (0)