Skip to content

Commit

Permalink
chore: automation-related cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@plt-amy
plt-amy committed Nov 29, 2023
1 parent 24d120f commit 8026cd6
Show file tree
Hide file tree
Showing 2 changed files with 81 additions and 98 deletions.
73 changes: 33 additions & 40 deletions src/Order/Base.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,31 +79,32 @@ instance
Underlying-Poset .Underlying.ℓ-underlying = _
Underlying-Poset .Underlying.⌞_⌟ = Poset.Ob

instance
open hlevel-projection

Poset-ob-hlevel-proj : hlevel-projection (quote Poset.Ob)
Poset-ob-hlevel-proj .hlevel-projection.has-level = quote Poset.Ob-is-set
Poset-ob-hlevel-proj .hlevel-projection.get-level _ = pure (lit (nat 2))
Poset-ob-hlevel-proj .hlevel-projection.get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
Poset-ob-hlevel-proj .hlevel-projection.get-argument _ = typeError []
Poset-ob-hlevel-proj .has-level = quote Poset.Ob-is-set
Poset-ob-hlevel-proj .get-level _ = pure (lit (nat 2))
Poset-ob-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
Poset-ob-hlevel-proj .get-argument _ = typeError []

Poset-≤-hlevel-proj : hlevel-projection (quote Poset._≤_)
Poset-≤-hlevel-proj .hlevel-projection.has-level = quote Poset.≤-thin
Poset-≤-hlevel-proj .hlevel-projection.get-level _ = pure (lit (nat 1))
Poset-≤-hlevel-proj .hlevel-projection.get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
Poset-≤-hlevel-proj .hlevel-projection.get-argument _ = typeError []
Poset-≤-hlevel-proj .has-level = quote Poset.≤-thin
Poset-≤-hlevel-proj .get-level _ = pure (lit (nat 1))
Poset-≤-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
Poset-≤-hlevel-proj .get-argument _ = typeError []
```
-->

```agda
record Monotone
{o o' ℓ ℓ'}
(P : Poset o ℓ) (Q : Poset o' ℓ')
: Type (o ⊔ o' ⊔ ℓ ⊔ ℓ')
where
record
Monotone {o o' ℓ ℓ'} (P : Poset o ℓ) (Q : Poset o' ℓ')
: Type (o ⊔ o' ⊔ ℓ ⊔ ℓ') where
no-eta-equality

private
module P = Poset P
module Q = Poset Q

field
hom : P.Ob → Q.Ob
pres-≤ : ∀ {x y} → x P.≤ y → hom x Q.≤ hom y
Expand All @@ -120,25 +121,15 @@ private

Monotone-is-hlevel : ∀ n → is-hlevel (Monotone P Q) (2 + n)
Monotone-is-hlevel {Q = Q} n =
Iso→is-hlevel (2 + n) eqv $
Σ-is-hlevel (2 + n) (Π-is-hlevel (2 + n) λ _ → is-set→is-hlevel+2 Q.Ob-is-set) λ _ →
Π-is-hlevel' (2 + n) λ _ → Π-is-hlevel' (2 + n) λ _ → Π-is-hlevel (2 + n) λ _ →
is-prop→is-hlevel-suc {n = suc n} Q.≤-thin
where
unquoteDecl eqv = declare-record-iso eqv (quote Monotone)
module Q = Poset Q
Iso→is-hlevel (2 + n) eqv $ is-set→is-hlevel+2 $ hlevel!
where unquoteDecl eqv = declare-record-iso eqv (quote Monotone)

instance
H-Level-Monotone
: ∀ {n}
→ H-Level (Monotone P Q) (2 + n)
H-Level-Monotone : ∀ {n} → H-Level (Monotone P Q) (2 + n)
H-Level-Monotone = basic-instance 2 (Monotone-is-hlevel 0)

instance
Funlike-Monotone : ∀ {o o' ℓ ℓ'} → Funlike (Monotone {o} {o'} {ℓ} {ℓ'})
Funlike-Monotone .Funlike.au = Underlying-Poset
Funlike-Monotone .Funlike.bu = Underlying-Poset
Funlike-Monotone .Funlike._#_ = hom
Funlike-Monotone = record { _#_ = hom }

Monotone-pathp
: ∀ {o ℓ o' ℓ'} {P : I → Poset o ℓ} {Q : I → Poset o' ℓ'}
Expand All @@ -151,17 +142,17 @@ Monotone-pathp {P = P} {Q} {f} {g} q i .Monotone.pres-≤ {x} {y} α =
(λ i → Π-is-hlevel³ {A = ⌞ P i ⌟} {B = λ _ → ⌞ P i ⌟} {C = λ x y → P i .Poset._≤_ x y} 1
λ x y _ → Q i .Poset.≤-thin {q i x} {q i y})
(λ _ _ α → f .Monotone.pres-≤ α)
(λ _ _ α → g .Monotone.pres-≤ α) i x y α
(λ _ _ α → g .Monotone.pres-≤ α) i x y α

Extensional-Monotone
: ∀ {o ℓ o' ℓ' ℓr} {P : Poset o ℓ} {Q : Poset o' ℓ'}
→ ⦃ sq : Extensional (⌞ Q ⌟) ℓr ⦄
→ Extensional (Monotone P Q) (o ⊔ ℓr)
→ ⦃ sa : Extensional (⌞ P ⌟ → ⌞ Q ⌟) ℓr ⦄
→ Extensional (Monotone P Q) ℓr
Extensional-Monotone {Q = Q} ⦃ sq ⦄ =
injection→extensional! Monotone-pathp (Extensional-→ ⦃ sq ⦄)
injection→extensional! Monotone-pathp sq

instance
Extensionality-Monotone
Extensionality-Monotone
: ∀ {o ℓ o' ℓ'} {P : Poset o ℓ} {Q : Poset o' ℓ'}
→ Extensionality (Monotone P Q)
Extensionality-Monotone = record { lemma = quote Extensional-Monotone }
Expand All @@ -170,21 +161,23 @@ instance

```agda
idₘ : Monotone P P
idₘ .hom x = x
idₘ .hom x = x
idₘ .pres-≤ x≤y = x≤y

_∘ₘ_ : Monotone Q R → Monotone P Q → Monotone P R
(f ∘ₘ g) .hom x = f # (g # x)
(f ∘ₘ g) .hom x = f # (g # x)
(f ∘ₘ g) .pres-≤ x≤y = f .pres-≤ (g .pres-≤ x≤y)

Posets : ∀ (o ℓ : Level) → Precategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ)
Posets o ℓ .Precategory.Ob = Poset o ℓ
Posets o ℓ .Precategory.Hom = Monotone
Posets o ℓ .Precategory.Ob = Poset o ℓ
Posets o ℓ .Precategory.Hom = Monotone
Posets o ℓ .Precategory.Hom-set = hlevel!
Posets o ℓ .Precategory.id = idₘ

Posets o ℓ .Precategory.id = idₘ
Posets o ℓ .Precategory._∘_ = _∘ₘ_
Posets o ℓ .Precategory.idr f = trivial!
Posets o ℓ .Precategory.idl f = trivial!

Posets o ℓ .Precategory.idr f = trivial!
Posets o ℓ .Precategory.idl f = trivial!
Posets o ℓ .Precategory.assoc f g h = trivial!
```

Expand Down
106 changes: 48 additions & 58 deletions src/Order/Univalent.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,71 +17,61 @@ module Order.Univalent where

# The Category of Posets is Univalent

<!--
```agda
module _ {o ℓ} {P Q : Poset o ℓ} where
private
module P = Poset P
module Q = Poset Q
```
-->

```agda
Poset-path : P Posets.≅ Q → P ≡ Q
Poset-path f = path
where
open Posets

P≃Q : ⌞ P ⌟ ≃ ⌞ Q ⌟
P≃Q = iso→equiv (F-map-iso Forget-poset f)
Poset-path : ∀ {o ℓ} {P Q : Poset o ℓ} → P Posets.≅ Q → P ≡ Q
Poset-path {P = P} {Q} f = path where
module P = Poset P
module Q = Poset Q
open Posets

ob : ∀ i → Type o
ob i = ua P≃Q i
P≃Q : ⌞ P ⌟ ≃ ⌞ Q ⌟
P≃Q = iso→equiv (F-map-iso Forget-poset f)

sys : ∀ i (x y : ob i) → Partial (i ∨ ~ i) _
sys i x y (i = i0) = (x P.≤ y) , iso→≤-equiv f
sys i x y (i = i1) = (x Q.≤ y) , (λ x → x) , id-equiv
ob : ∀ i → Type _
ob i = ua P≃Q i

order : PathP (λ i → ob i → ob i → Type ℓ) P._≤_ Q._≤_
order i x y = Glue ((unglue (i ∨ ~ i) x) Q.≤ (unglue (i ∨ ~ i) y)) (sys i x y)
order : PathP (λ i → ob i → ob i → Type _) P._≤_ Q._≤_
order i x y = Glue (unglue (∂ i) x Q.≤ unglue (∂ i) y) λ where
(i = i0) → x P.≤ y , iso→≤-equiv f
(i = i1) → x Q.≤ y , _ , id-equiv

order-thin : ∀ i x y → is-prop (order i x y)
order-thin i = coe0→i (λ i → (x y : ob i) → is-prop (order i x y)) i hlevel!
order-thin : ∀ i x y → is-prop (order i x y)
order-thin i = coe0→i (λ i → (x y : ob i) → is-prop (order i x y)) i hlevel!

ob-set : ∀ i → is-set (ob i)
ob-set i = coe0→i (λ i → is-set (ob i)) i hlevel!
ob-set : ∀ i → is-set (ob i)
ob-set i = coe0→i (λ i → is-set (ob i)) i hlevel!

path : P ≡ Q
path i .Poset.Ob = ob i
path i .Poset._≤_ x y = order i x y
path i .Poset.≤-thin {x} {y} =
is-prop→pathp
(λ i →
Π-is-hlevel² {A = ob i} {B = λ _ → ob i} 1 λ x y →
is-prop-is-prop {A = order i x y})
(λ _ _ → P.≤-thin)
(λ _ _ → Q.≤-thin) i x y
path i .Poset.≤-refl {x = x} =
is-prop→pathp
(λ i → Π-is-hlevel {A = ob i} 1 λ x → order-thin i x x)
(λ _ → P.≤-refl)
(λ _ → Q.≤-refl) i x
path i .Poset.≤-trans {x} {y} {z} x≤y y≤z =
is-prop→pathp
(λ i →
Π-is-hlevel³ {A = ob i} {B = λ _ → ob i} {C = λ _ _ → ob i} 1 λ x y z →
Π-is-hlevel² {A = order i x y} {B = λ _ → order i y z} 1 λ _ _ →
order-thin i x z)
(λ _ _ _ → P.≤-trans)
(λ _ _ _ → Q.≤-trans) i x y z x≤y y≤z
path i .Poset.≤-antisym {x} {y} x≤y y≤x =
is-prop→pathp
(λ i →
Π-is-hlevel² {A = ob i } {B = λ _ → ob i} 1 λ x y →
Π-is-hlevel² {A = order i x y} {B = λ _ → order i y x} 1 λ _ _ →
ob-set i x y)
(λ _ _ → P.≤-antisym)
(λ _ _ → Q.≤-antisym) i x y x≤y y≤x
path : P ≡ Q
path i .Poset.Ob = ob i
path i .Poset._≤_ x y = order i x y
path i .Poset.≤-thin {x} {y} =
is-prop→pathp
(λ i →
Π-is-hlevel² {A = ob i} {B = λ _ → ob i} 1 λ x y →
is-prop-is-prop {A = order i x y})
(λ _ _ → P.≤-thin)
(λ _ _ → Q.≤-thin) i x y
path i .Poset.≤-refl {x = x} =
is-prop→pathp
(λ i → Π-is-hlevel {A = ob i} 1 λ x → order-thin i x x)
(λ _ → P.≤-refl)
(λ _ → Q.≤-refl) i x
path i .Poset.≤-trans {x} {y} {z} x≤y y≤z =
is-prop→pathp
(λ i →
Π-is-hlevel³ {A = ob i} {B = λ _ → ob i} {C = λ _ _ → ob i} 1 λ x y z →
Π-is-hlevel² {A = order i x y} {B = λ _ → order i y z} 1 λ _ _ →
order-thin i x z)
(λ _ _ _ → P.≤-trans)
(λ _ _ _ → Q.≤-trans) i x y z x≤y y≤z
path i .Poset.≤-antisym {x} {y} x≤y y≤x =
is-prop→pathp
(λ i →
Π-is-hlevel² {A = ob i } {B = λ _ → ob i} 1 λ x y →
Π-is-hlevel² {A = order i x y} {B = λ _ → order i y x} 1 λ _ _ →
ob-set i x y)
(λ _ _ → P.≤-antisym)
(λ _ _ → Q.≤-antisym) i x y x≤y y≤x
```

```agda
Expand Down

0 comments on commit 8026cd6

Please sign in to comment.