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

add Bool.elim #996

Merged
merged 1 commit into from
Jun 1, 2023
Merged

add Bool.elim #996

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
15 changes: 11 additions & 4 deletions Cubical/Data/Bool/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,14 @@ open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Pointed

open import Cubical.Data.Sum
open import Cubical.Data.Sum hiding (elim)
open import Cubical.Data.Bool.Base
open import Cubical.Data.Empty
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Empty hiding (elim)
open import Cubical.Data.Empty as Empty hiding (elim)
open import Cubical.Data.Sigma
open import Cubical.Data.Unit using (Unit; isPropUnit)

open import Cubical.HITs.PropositionalTruncation hiding (rec)
open import Cubical.HITs.PropositionalTruncation hiding (elim; rec)

open import Cubical.Relation.Nullary

Expand All @@ -30,6 +30,13 @@ private
ℓ : Level
A : Type ℓ

elim : ∀ {ℓ} {A : Bool → Type ℓ}
→ A true
→ A false
→ (b : Bool) → A b
elim t f false = f
elim t f true = t

notnot : ∀ x → not (not x) ≡ x
notnot true = refl
notnot false = refl
Expand Down
2 changes: 1 addition & 1 deletion Cubical/HITs/RPn/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ open import Cubical.Foundations.SIP
open import Cubical.Structures.Pointed
open import Cubical.Structures.TypeEqvTo

open import Cubical.Data.Bool
open import Cubical.Data.Bool hiding (elim)
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.NatMinusOne
open import Cubical.Data.Sigma
Expand Down
2 changes: 1 addition & 1 deletion Cubical/HITs/Sn/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ open import Cubical.HITs.Susp renaming (toSusp to σ)
open import Cubical.HITs.Truncation
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Join renaming (joinS¹S¹→S³ to joinS¹S¹→S3)
open import Cubical.Data.Bool
open import Cubical.Data.Bool hiding (elim)

private
variable
Expand Down
2 changes: 1 addition & 1 deletion Cubical/HITs/Truncation/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ open Modality

open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool
open import Cubical.Data.Bool hiding (elim)
open import Cubical.Data.Unit
open import Cubical.HITs.Sn.Base
open import Cubical.HITs.S1 hiding (rec ; elim)
Expand Down