<commit_before>{-# OPTIONS --without-K #-}
open import Data.Two hiding (_≟_; decSetoid)
open import Type
open import Relation.Binary
open import Relation.Nullary
open import Function
import Relation.Binary.PropositionalEquality as ≡
open ≡ using (_≡_)

module Data.Two.Equality where

module ✓-== where

    decSetoid : DecSetoid _ _
    decSetoid = record { Carrier = 𝟚; _≈_ = _≈_; isDecEquivalence = isDecEquivalence }
      where
        _≈_ : (x y : 𝟚) → ★₀
        x ≈ y = ✓ (x == y)

        refl : Reflexive _≈_
        refl {0₂} = _
        refl {1₂} = _

        subst : ∀ {ℓ} → Substitutive _≈_ ℓ
        subst _ {0₂} {0₂} _ = id
        subst _ {1₂} {1₂} _ = id
        subst _ {0₂} {1₂} ()
        subst _ {1₂} {0₂} ()

        sym : Symmetric _≈_
        sym {x} {y} eq = subst (λ y → y ≈ x) {x} {y} eq (refl {x})

        trans : Transitive _≈_
        trans {x} {y} {z} x≈y y≈z = subst (_≈_ x) {y} {z} y≈z x≈y

        _≟_ : Decidable _≈_
        0₂ ≟ 0₂ = yes _
        1₂ ≟ 1₂ = yes _
        0₂ ≟ 1₂ = no (λ())
        1₂ ≟ 0₂ = no (λ())

        isEquivalence : IsEquivalence _≈_
        isEquivalence = record { refl  = λ {x} → refl {x}
                               ; sym   = λ {x} {y} → sym {x} {y}
                               ; trans = λ {x} {y} {z} → trans {x} {y} {z} }

        isDecEquivalence : IsDecEquivalence _≈_
        isDecEquivalence = record { isEquivalence = isEquivalence; _≟_ = _≟_ }

    open DecSetoid decSetoid public hiding (_≈_; _≟_)

module ==-≡1₂ where

    decSetoid : DecSetoid _ _
    decSetoid = record { Carrier = 𝟚; _≈_ = _≈_; isDecEquivalence = isDecEquivalence }
      where
        _≈_ : (x y : 𝟚) → ★₀
        x ≈ y = (x == y) ≡ 1₂

        refl : Reflexive _≈_
        refl {0₂} = ≡.refl
        refl {1₂} = ≡.refl

        subst : ∀ {ℓ} → Substitutive _≈_ ℓ
        subst _ {0₂} {0₂} _ = id
        subst _ {1₂} {1₂} _ = id
        subst _ {0₂} {1₂} ()
        subst _ {1₂} {0₂} ()

        sym : Symmetric _≈_
        sym {x} {y} eq = subst (λ y → y ≈ x) {x} {y} eq (refl {x})

        trans : Transitive _≈_
        trans {x} x≈y y≈z = subst (_≈_ x) y≈z x≈y

        _≟_ : Decidable _≈_
        0₂ ≟ 0₂ = yes ≡.refl
        1₂ ≟ 1₂ = yes ≡.refl
        0₂ ≟ 1₂ = no (λ())
        1₂ ≟ 0₂ = no (λ())

        isEquivalence : IsEquivalence _≈_
        isEquivalence = record { refl  = λ {x} → refl {x}
                               ; sym   = λ {x} {y} → sym {x} {y}
                               ; trans = λ {x} {y} {z} → trans {x} {y} {z} }

        isDecEquivalence : IsDecEquivalence _≈_
        isDecEquivalence = record { isEquivalence = isEquivalence; _≟_ = _≟_ }

    open DecSetoid decSetoid public

neg-xor : ∀ b₀ b₁ → b₀ == b₁ ≡ not (b₀ xor b₁)
neg-xor 0₂ b = ≡.refl
neg-xor 1₂ b = ≡.sym (not-involutive b)

comm : ∀ b₀ b₁ → b₀ == b₁ ≡ b₁ == b₀
comm 0₂ 0₂ = ≡.refl
comm 0₂ 1₂ = ≡.refl
comm 1₂ 0₂ = ≡.refl
comm 1₂ 1₂ = ≡.refl
<commit_msg>Two.Equality: export subst and ⇒≡<commit_after>{-# OPTIONS --without-K #-}
open import Data.Two hiding (_≟_; decSetoid)
open import Type
open import Relation.Binary.NP
open import Relation.Nullary
open import Function
import Relation.Binary.PropositionalEquality as ≡
open ≡ using (_≡_)

module Data.Two.Equality where

module ✓-== where

    _≈_ : (x y : 𝟚) → ★₀
    x ≈ y = ✓ (x == y)

    subst : ∀ {ℓ} → Substitutive _≈_ ℓ
    subst _ {0₂} {0₂} _ = id
    subst _ {1₂} {1₂} _ = id
    subst _ {0₂} {1₂} ()
    subst _ {1₂} {0₂} ()

    ⇒≡ : _≈_ ⇒ _≡_
    ⇒≡ = substitutive⇒≡ subst

    decSetoid : DecSetoid _ _
    decSetoid = record { Carrier = 𝟚; _≈_ = _≈_; isDecEquivalence = isDecEquivalence }
      where
        refl : Reflexive _≈_
        refl {0₂} = _
        refl {1₂} = _

        sym : Symmetric _≈_
        sym {x} {y} eq = subst (λ y → y ≈ x) {x} {y} eq (refl {x})

        trans : Transitive _≈_
        trans {x} {y} {z} x≈y y≈z = subst (_≈_ x) {y} {z} y≈z x≈y

        _≟_ : Decidable _≈_
        0₂ ≟ 0₂ = yes _
        1₂ ≟ 1₂ = yes _
        0₂ ≟ 1₂ = no (λ())
        1₂ ≟ 0₂ = no (λ())

        isEquivalence : IsEquivalence _≈_
        isEquivalence = record { refl  = λ {x} → refl {x}
                               ; sym   = λ {x} {y} → sym {x} {y}
                               ; trans = λ {x} {y} {z} → trans {x} {y} {z} }

        isDecEquivalence : IsDecEquivalence _≈_
        isDecEquivalence = record { isEquivalence = isEquivalence; _≟_ = _≟_ }

    open DecSetoid decSetoid public hiding (_≈_)

module ==-≡1₂ where

    _≈_ : (x y : 𝟚) → ★₀
    x ≈ y = (x == y) ≡ 1₂

    subst : ∀ {ℓ} → Substitutive _≈_ ℓ
    subst _ {0₂} {0₂} _ = id
    subst _ {1₂} {1₂} _ = id
    subst _ {0₂} {1₂} ()
    subst _ {1₂} {0₂} ()

    ⇒≡ : _≈_ ⇒ _≡_
    ⇒≡ = substitutive⇒≡ subst

    decSetoid : DecSetoid _ _
    decSetoid = record { Carrier = 𝟚; _≈_ = _≈_; isDecEquivalence = isDecEquivalence }
      where
        refl : Reflexive _≈_
        refl {0₂} = ≡.refl
        refl {1₂} = ≡.refl

        sym : Symmetric _≈_
        sym {x} {y} eq = subst (λ y → y ≈ x) {x} {y} eq (refl {x})

        trans : Transitive _≈_
        trans {x} x≈y y≈z = subst (_≈_ x) y≈z x≈y

        _≟_ : Decidable _≈_
        0₂ ≟ 0₂ = yes ≡.refl
        1₂ ≟ 1₂ = yes ≡.refl
        0₂ ≟ 1₂ = no (λ())
        1₂ ≟ 0₂ = no (λ())

        isEquivalence : IsEquivalence _≈_
        isEquivalence = record { refl  = λ {x} → refl {x}
                               ; sym   = λ {x} {y} → sym {x} {y}
                               ; trans = λ {x} {y} {z} → trans {x} {y} {z} }

        isDecEquivalence : IsDecEquivalence _≈_
        isDecEquivalence = record { isEquivalence = isEquivalence; _≟_ = _≟_ }

    open DecSetoid decSetoid public hiding (_≈_)

neg-xor : ∀ b₀ b₁ → b₀ == b₁ ≡ not (b₀ xor b₁)
neg-xor 0₂ b = ≡.refl
neg-xor 1₂ b = ≡.sym (not-involutive b)

comm : ∀ b₀ b₁ → b₀ == b₁ ≡ b₁ == b₀
comm 0₂ 0₂ = ≡.refl
comm 0₂ 1₂ = ≡.refl
comm 1₂ 0₂ = ≡.refl
comm 1₂ 1₂ = ≡.refl

{'fraction_non_alphanumeric': 0.14481939969476004, 'fraction_numerical': 0.01763608614549771, 'mean_word_length': 1.7179723502304147, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2853558', 'n_tokens_mistral': 2694, 'n_tokens_neox': 2706, 'n_words': 795}