Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}

module foundations.DecidableEquality where
open import foundations.TransportLemmas
open import foundations.ProductIdentities
open import foundations.EquivalenceType
open import foundations.HomotopyType

A type has decidable equality if any two of its elements are equal or different. This would be a particular instance of the Law of Excluded Middle that holds even if we do not assume Excluded Middle.

module DecidableEquality where

decEq
  : ∀ {ℓ : Level} → (A : Type ℓ) → Type ℓ

decEq A = (a b : A) → (a ≡ b) + (a ≠ b)

and a more convenient name for this:

_is-decidable
  : ∀ {ℓ : Level} → (A : Type ℓ) → Type ℓ
A is-decidable = decEq A

The product of types with decidable equality is a type with decidable equality.

decEqProd
  : ∀ {ℓ : Level} {A B : Type ℓ}
  → decEq A → decEq B
  -------------------
  → decEq (A × B)

decEqProd da db (a1 , b1) (a2 , b2)
 with (da a1 a2) | (db b1 b2)
... | inl aeq | inl beq = inl (prodByComponents (aeq , beq))
... | inl _   | inr bnq = inr λ b → bnq (ap π₂ b)
... | inr anq | _       = inr λ b → anq (ap π₁ b)

This surely can be extend to other types.

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides