Intervals in posets and the covering relation #1219

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged

mortberg merged 20 commits into agda:master from anshwad10:oriented-graded-posets

Aug 1, 2025

Cubical/Functions/Embedding.agda

-Original file line number
+Diff line change
@@ Expand Up / @@ -191,6 +191,10 @@ iso→isEmbedding : ∀ {ℓ} {A B : Type ℓ} @@
       → isEmbedding (Iso.fun isom)
     iso→isEmbedding {A = A} {B} isom = (isEquiv→isEmbedding (equivIsEquiv (isoToEquiv isom)))
+    Iso→Embedding : ∀ {ℓ} {A B : Type ℓ}
+      → Iso A B → A ↪ B
+    Iso→Embedding isom = _ , iso→isEmbedding isom
     isEmbedding→Injection :
       ∀ {ℓ} {A B C : Type ℓ}
       → (a : A → B)
@@ Expand Down @@

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

-Original file line number
+Diff line change
@@ -0,0 +1,81 @@
+    -- The covering relation
+    {-# OPTIONS --safe #-}
+    module Cubical.Relation.Binary.Order.Poset.Covering where
+    open import Cubical.Foundations.Equiv
+    open import Cubical.Foundations.HLevels
+    open import Cubical.Foundations.Isomorphism
+    open import Cubical.Foundations.Prelude
+    open import Cubical.Foundations.Function
+    open import Cubical.Foundations.Structure
+    open import Cubical.Foundations.Transport
+    open import Cubical.Functions.Embedding
+    open import Cubical.Functions.Fibration
+    open import Cubical.Data.Bool as B using (Bool; true; false)
+    open import Cubical.Data.Sum as ⊎
+    open import Cubical.Data.Empty as ⊥
+    open import Cubical.Relation.Binary.Order.Poset.Base
+    open import Cubical.Relation.Binary.Order.Poset.Properties
+    open import Cubical.Relation.Binary.Order.Poset.Subset
+    open import Cubical.Relation.Binary.Order.Poset.Interval
+    open import Cubical.Relation.Nullary
+    open import Cubical.Reflection.RecordEquiv
+    private variable
+      ℓ ℓ' : Level
+    module Cover (P' : Poset ℓ ℓ') where
+      private P = ⟨ P' ⟩
+      open PosetStr (snd P')
+      infixl 20 _covers_
+      _covers_ : P → P → Type (ℓ-max ℓ ℓ')
+      y covers x = Σ[ x≤y ∈ x ≤ y ] isEquiv (2→Interval P' x y x≤y)
+      isPropCovers : ∀ y x → isProp (y covers x)
+      isPropCovers y x = isPropΣ (is-prop-valued x y) (λ _ → isPropIsEquiv _)
+      module _ (x y : P) (x≤y : x ≤ y) (x≠y : ¬ x ≡ y)
+               (cov : ∀ z → x ≤ z → z ≤ y → (z ≡ x) ⊎ (z ≡ y)) where
+        open Iso
+        private
+          cov' : (i : Interval P' x y) → (i .Interval.z ≡ x) ⊎ (i .Interval.z ≡ y)
+          cov' (interval z x≤z z≤y) = cov z x≤z z≤y
+        makeCovers : y covers x
+        makeCovers = x≤y , isoToIsEquiv isom where
+          isom : Iso Bool (Interval P' x y)
+          isom .fun = 2→Interval P' x y x≤y
+          isom .inv i with cov' i
+          ... | inl z≡x = false
+          ... | inr z≡y = true
+          isom .rightInv i with cov' i
+          ... | inl z≡x = Interval≡ P' x y _ _ (sym z≡x)
+          ... | inr z≡y = Interval≡ P' x y _ _ (sym z≡y)
+          isom .leftInv b with cov' (2→Interval P' x y x≤y b)
+          isom .leftInv false | inl _ = refl
+          isom .leftInv false | inr x≡y = ⊥.rec (x≠y x≡y)
+          isom .leftInv true  | inl y≡x = ⊥.rec (x≠y (sym y≡x))
+          isom .leftInv true  | inr _ = refl
+      -- Subset of faces and cofaces
+      -- terminology from "Combinatorics of higher-categorical diagrams" by Amar Hadzihasanovic
+      Δ : P → Embedding P (ℓ-max ℓ ℓ')
+      Δ x = (Σ[ y ∈ P ] x covers y) , EmbeddingΣProp λ _ → isPropCovers _ _
+      ∇ : P → Embedding P (ℓ-max ℓ ℓ')
+      ∇ x = (Σ[ y ∈ P ] y covers x) , EmbeddingΣProp λ _ → isPropCovers _ _
+      ΔMembership : ∀ x y → x covers y ≃ y ∈ₑ Δ x
+      ΔMembership x y = invEquiv (fiberEquiv _ _)
+      ∇Membership : ∀ x y → y covers x ≃ y ∈ₑ ∇ x
+      ∇Membership x y = invEquiv (fiberEquiv _ _)

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

-Original file line number
+Diff line change
@@ -0,0 +1,71 @@
+    {-# OPTIONS --safe #-}
+    module Cubical.Relation.Binary.Order.Poset.Interval where
+    open import Cubical.Foundations.Equiv
+    open import Cubical.Foundations.HLevels
+    open import Cubical.Foundations.Prelude
+    open import Cubical.Foundations.Function
+    open import Cubical.Foundations.Structure
+    open import Cubical.Foundations.Transport
+    open import Cubical.Foundations.Isomorphism
+    open import Cubical.Functions.Embedding
+    open import Cubical.Functions.Fibration
+    open import Cubical.Data.Bool as B using (Bool; true; false)
+    open import Cubical.Data.Sigma
+    open import Cubical.Relation.Binary.Order.Poset.Base
+    open import Cubical.Relation.Binary.Order.Poset.Properties
+    open import Cubical.Relation.Binary.Order.Poset.Subset
+    open import Cubical.Reflection.RecordEquiv
+    private variable
+      ℓ ℓ' : Level
+    module _ (P' : Poset ℓ ℓ') where
+      private P = ⟨ P' ⟩
+      open PosetStr (snd P')
+      module _ (x y : P) where
+        -- the set of elements between x and y
+        record Interval : Type (ℓ-max ℓ ℓ') where
+          constructor interval
+          field
+            z : P
+            x≤z : x ≤ z
+            z≤y : z ≤ y
+        unquoteDecl IntervalIsoΣ = declareRecordIsoΣ IntervalIsoΣ (quote Interval)
+        isSetInterval : isSet Interval
+        isSetInterval = isOfHLevelRetractFromIso 2 IntervalIsoΣ $
+          isSetΣSndProp is-set λ _ → isProp× (is-prop-valued _ _) (is-prop-valued _ _)
+        Interval↪ : Interval ↪ P
+        Interval↪ = compEmbedding (EmbeddingΣProp λ _ → isProp× (is-prop-valued _ _) (is-prop-valued _ _)) (Iso→Embedding IntervalIsoΣ)
+        IntervalEmbedding : Embedding P (ℓ-max ℓ ℓ')
+        IntervalEmbedding = Interval , Interval↪
+        IntervalPosetStr : PosetStr ℓ' Interval
+        IntervalPosetStr = posetstr _ (isPosetInduced isPoset Interval Interval↪)
+        IntervalPoset : Poset (ℓ-max ℓ ℓ') ℓ'
+        IntervalPoset = Interval , IntervalPosetStr
+        Interval≡ : ∀ i j → i .Interval.z ≡ j .Interval.z → i ≡ j
+        Interval≡ _ _ = isoFunInjective IntervalIsoΣ _ _ ∘ Σ≡Prop (λ _ → isProp× (is-prop-valued _ _) (is-prop-valued _ _))
+        module _ (x≤y : x ≤ y) where
+          intervalTop : Interval
+          intervalTop = interval y x≤y (is-refl y)
+          intervalBot : Interval
+          intervalBot = interval x (is-refl x) x≤y
+→Interval : Bool → Interval
+→Interval false = intervalBot
+→Interval true  = intervalTop

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Intervals in posets and the covering relation #1219

Uh oh!

Diff view

Diff view

There are no files selected for viewing