Skip to content
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.

Sign up for GitHub

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

Deprecating Relation.Binary.PropositionalEquality.isPropositional #2205

Merged
merged 3 commits into from
Nov 21, 2023
Merged

Deprecating Relation.Binary.PropositionalEquality.isPropositional #2205

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c5bf817
deprecating `isPropositional`
jamesmckinna Nov 17, 2023
e50e171
tighten `import`s
jamesmckinna Nov 17, 2023
f2ee05f
bumped Agda version number in comment
jamesmckinna Nov 17, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1727,6 +1727,11 @@ Deprecated names
invPreorder ↦ converse-preorder
```

* In `Relation.Binary.PropositionalEquality`:
```agda
isPropositional ↦ Relation.Nullary.Irrelevant
```

* In `Relation.Unary.Consequences`:
```agda
dec⟶recomputable ↦ dec⇒recomputable
Expand Down
31 changes: 21 additions & 10 deletions src/Relation/Binary/PropositionalEquality.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,12 @@

module Relation.Binary.PropositionalEquality where

import Axiom.Extensionality.Propositional as Ext
open import Axiom.UniquenessOfIdentityProofs
open import Function.Base using (id; _∘_)
import Function.Dependent.Bundles as Dependent
open import Function.Indexed.Relation.Binary.Equality using (≡-setoid)
open import Level using (Level; _⊔_)
open import Data.Product.Base using (∃)

open import Relation.Nullary using (Irrelevant)
open import Relation.Nullary.Decidable using (yes; no; dec-yes-irr; dec-no)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (DecidableEquality)
Expand Down Expand Up @@ -60,12 +58,6 @@ _≗_ {A = A} {B = B} = Setoid._≈_ (A →-setoid B)
Dependent.Func (setoid A) (Trivial.indexedSetoid B)
→-to-⟶ = :→-to-Π

------------------------------------------------------------------------
-- Propositionality

isPropositional : Set a → Set a
isPropositional A = (a b : A) → a ≡ b

------------------------------------------------------------------------
-- More complex rearrangement lemmas

Expand Down Expand Up @@ -113,7 +105,7 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where
-- See README.Inspect for an explanation of how/why to use this.

-- Normally (but not always) the new `with ... in` syntax described at
-- https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality
-- https://agda.readthedocs.io/en/v2.6.4/language/with-abstraction.html#with-abstraction-equality
-- can be used instead."

record Reveal_·_is_ {A : Set a} {B : A → Set b}
Expand All @@ -125,3 +117,22 @@ record Reveal_·_is_ {A : Set a} {B : A → Set b}
inspect : ∀ {A : Set a} {B : A → Set b}
(f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]


------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

isPropositional : Set a → Set a
isPropositional = Irrelevant

{-# WARNING_ON_USAGE isPropositional
"Warning: isPropositional was deprecated in v2.0.
Please use Relation.Nullary.Irrelevant instead. "
#-}


Loading