text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Algebra

module Algebra.Properties.BooleanAlgebra
  {b₁ b₂} (B : BooleanAlgebra b₁ b₂)
  where

open BooleanAlgebra B
import Algebra.Properties.DistributiveLattice
private
  open module DL = Algebra.Properties.DistributiveLattice
                     distributiveLattice public
    hiding (replace-equality)
open import Algebra.Structures _≈_
open import Algebra.FunctionProperties _≈_
open import Algebra.FunctionProperties.Consequences setoid
open import Relation.Binary.Reasoning.Setoid setoid
open import Relation.Binary
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Data.Product using (_,_)

------------------------------------------------------------------------
-- Some simple generalisations

∨-complementˡ : LeftInverse ⊤ ¬_ _∨_
∨-complementˡ = comm+invʳ⇒invˡ ∨-comm ∨-complementʳ

∨-complement : Inverse ⊤ ¬_ _∨_
∨-complement = ∨-complementˡ , ∨-complementʳ

∧-complementˡ : LeftInverse ⊥ ¬_ _∧_
∧-complementˡ = comm+invʳ⇒invˡ ∧-comm ∧-complementʳ

∧-complement : Inverse ⊥ ¬_ _∧_
∧-complement = ∧-complementˡ , ∧-complementʳ

------------------------------------------------------------------------
-- The dual construction is also a boolean algebra

∧-∨-isBooleanAlgebra : IsBooleanAlgebra _∧_ _∨_ ¬_ ⊥ ⊤
∧-∨-isBooleanAlgebra = record
  { isDistributiveLattice = ∧-∨-isDistributiveLattice
  ; ∨-complementʳ         = ∧-complementʳ
  ; ∧-complementʳ         = ∨-complementʳ
  ; ¬-cong                = ¬-cong
  }

∧-∨-booleanAlgebra : BooleanAlgebra _ _
∧-∨-booleanAlgebra = record
  { _∧_              = _∨_
  ; _∨_              = _∧_
  ; ⊤                = ⊥
  ; ⊥                = ⊤
  ; isBooleanAlgebra = ∧-∨-isBooleanAlgebra
  }

------------------------------------------------------------------------
-- (∨, ∧, ⊥, ⊤) and (∧, ∨, ⊤, ⊥) are commutative semirings

∧-identityʳ : RightIdentity ⊤ _∧_
∧-identityʳ x = begin
  x ∧ ⊤          ≈⟨ ∧-congˡ (sym (∨-complementʳ _)) ⟩
  x ∧ (x ∨ ¬ x)  ≈⟨ ∧-absorbs-∨ _ _ ⟩
  x              ∎

∧-identityˡ : LeftIdentity ⊤ _∧_
∧-identityˡ = comm+idʳ⇒idˡ ∧-comm ∧-identityʳ

∧-identity : Identity ⊤ _∧_
∧-identity = ∧-identityˡ , ∧-identityʳ

∨-identityʳ : RightIdentity ⊥ _∨_
∨-identityʳ x = begin
  x ∨ ⊥          ≈⟨ ∨-congˡ $ sym (∧-complementʳ _) ⟩
  x ∨ x ∧ ¬ x    ≈⟨ ∨-absorbs-∧ _ _ ⟩
  x              ∎

∨-identityˡ : LeftIdentity ⊥ _∨_
∨-identityˡ = comm+idʳ⇒idˡ ∨-comm ∨-identityʳ

∨-identity : Identity ⊥ _∨_
∨-identity = ∨-identityˡ , ∨-identityʳ

∧-zeroʳ : RightZero ⊥ _∧_
∧-zeroʳ x = begin
  x ∧ ⊥          ≈⟨ ∧-congˡ $ sym (∧-complementʳ _) ⟩
  x ∧  x  ∧ ¬ x  ≈˘⟨ ∧-assoc _ _ _ ⟩
  (x ∧ x) ∧ ¬ x  ≈⟨ ∧-congʳ $ ∧-idempotent _ ⟩
  x       ∧ ¬ x  ≈⟨ ∧-complementʳ _ ⟩
  ⊥              ∎

∧-zeroˡ : LeftZero ⊥ _∧_
∧-zeroˡ = comm+zeʳ⇒zeˡ ∧-comm ∧-zeroʳ

∧-zero : Zero ⊥ _∧_
∧-zero = ∧-zeroˡ , ∧-zeroʳ

∨-zeroʳ : ∀ x → x ∨ ⊤ ≈ ⊤
∨-zeroʳ x = begin
  x ∨ ⊤          ≈⟨ ∨-congˡ $ sym (∨-complementʳ _) ⟩
  x ∨  x  ∨ ¬ x  ≈˘⟨ ∨-assoc _ _ _ ⟩
  (x ∨ x) ∨ ¬ x  ≈⟨ ∨-congʳ $ ∨-idempotent _ ⟩
  x       ∨ ¬ x  ≈⟨ ∨-complementʳ _ ⟩
  ⊤              ∎

∨-zeroˡ : LeftZero ⊤ _∨_
∨-zeroˡ _ = ∨-comm _ _ ⟨ trans ⟩ ∨-zeroʳ _

∨-zero : Zero ⊤ _∨_
∨-zero = ∨-zeroˡ , ∨-zeroʳ

∨-isMagma : IsMagma _∨_
∨-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = ∨-cong
  }

∧-isMagma : IsMagma _∧_
∧-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = ∧-cong
  }

∨-isSemigroup : IsSemigroup _∨_
∨-isSemigroup = record
  { isMagma = ∨-isMagma
  ; assoc   = ∨-assoc
  }

∧-isSemigroup : IsSemigroup _∧_
∧-isSemigroup = record
  { isMagma = ∧-isMagma
  ; assoc   = ∧-assoc
  }

∨-⊥-isMonoid : IsMonoid _∨_ ⊥
∨-⊥-isMonoid = record
  { isSemigroup = ∨-isSemigroup
  ; identity    = ∨-identity
  }

∧-⊤-isMonoid : IsMonoid _∧_ ⊤
∧-⊤-isMonoid = record
  { isSemigroup = ∧-isSemigroup
  ; identity    = ∧-identity
  }

∨-⊥-isCommutativeMonoid : IsCommutativeMonoid _∨_ ⊥
∨-⊥-isCommutativeMonoid = record
  { isSemigroup = ∨-isSemigroup
  ; identityˡ   = ∨-identityˡ
  ; comm        = ∨-comm
  }

∧-⊤-isCommutativeMonoid : IsCommutativeMonoid _∧_ ⊤
∧-⊤-isCommutativeMonoid = record
  { isSemigroup = ∧-isSemigroup
  ; identityˡ   = ∧-identityˡ
  ; comm        = ∧-comm
  }

∨-∧-isCommutativeSemiring : IsCommutativeSemiring _∨_ _∧_ ⊥ ⊤
∨-∧-isCommutativeSemiring = record
  { +-isCommutativeMonoid = ∨-⊥-isCommutativeMonoid
  ; *-isCommutativeMonoid = ∧-⊤-isCommutativeMonoid
  ; distribʳ              = ∧-∨-distribʳ
  ; zeroˡ                 = ∧-zeroˡ
  }

∨-∧-commutativeSemiring : CommutativeSemiring _ _
∨-∧-commutativeSemiring = record
  { _+_                   = _∨_
  ; _*_                   = _∧_
  ; 0#                    = ⊥
  ; 1#                    = ⊤
  ; isCommutativeSemiring = ∨-∧-isCommutativeSemiring
  }

∧-∨-isCommutativeSemiring : IsCommutativeSemiring _∧_ _∨_ ⊤ ⊥
∧-∨-isCommutativeSemiring = record
  { +-isCommutativeMonoid = ∧-⊤-isCommutativeMonoid
  ; *-isCommutativeMonoid = ∨-⊥-isCommutativeMonoid
  ; distribʳ = ∨-∧-distribʳ
  ; zeroˡ    = ∨-zeroˡ
  }

∧-∨-commutativeSemiring : CommutativeSemiring _ _
∧-∨-commutativeSemiring = record
  { _+_                   = _∧_
  ; _*_                   = _∨_
  ; 0#                    = ⊤
  ; 1#                    = ⊥
  ; isCommutativeSemiring = ∧-∨-isCommutativeSemiring
  }

------------------------------------------------------------------------
-- Some other properties

-- I took the statement of this lemma (called Uniqueness of
-- Complements) from some course notes, "Boolean Algebra", written
-- by Gert Smolka.

private
  lemma : ∀ x y → x ∧ y ≈ ⊥ → x ∨ y ≈ ⊤ → ¬ x ≈ y
  lemma x y x∧y=⊥ x∨y=⊤ = begin
    ¬ x                ≈˘⟨ ∧-identityʳ _ ⟩
    ¬ x ∧ ⊤            ≈˘⟨ ∧-congˡ x∨y=⊤ ⟩
    ¬ x ∧ (x ∨ y)      ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
    ¬ x ∧ x ∨ ¬ x ∧ y  ≈⟨ ∨-congʳ $ ∧-complementˡ _ ⟩
    ⊥ ∨ ¬ x ∧ y        ≈˘⟨ ∨-congʳ x∧y=⊥ ⟩
    x ∧ y ∨ ¬ x ∧ y    ≈˘⟨ ∧-∨-distribʳ _ _ _ ⟩
    (x ∨ ¬ x) ∧ y      ≈⟨ ∧-congʳ $ ∨-complementʳ _ ⟩
    ⊤ ∧ y              ≈⟨ ∧-identityˡ _ ⟩
    y                  ∎

¬⊥=⊤ : ¬ ⊥ ≈ ⊤
¬⊥=⊤ = lemma ⊥ ⊤ (∧-identityʳ _) (∨-zeroʳ _)

¬⊤=⊥ : ¬ ⊤ ≈ ⊥
¬⊤=⊥ = lemma ⊤ ⊥ (∧-zeroʳ _) (∨-identityʳ _)

¬-involutive : Involutive ¬_
¬-involutive x = lemma (¬ x) x (∧-complementˡ _) (∨-complementˡ _)

deMorgan₁ : ∀ x y → ¬ (x ∧ y) ≈ ¬ x ∨ ¬ y
deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂
  where
  lem₁ = begin
    (x ∧ y) ∧ (¬ x ∨ ¬ y)          ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
    (x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ ∨-congʳ $ ∧-congʳ $ ∧-comm _ _ ⟩
    (y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ ∧-assoc _ _ _ ⟨ ∨-cong ⟩ ∧-assoc _ _ _ ⟩
    y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y)  ≈⟨ (∧-congˡ $ ∧-complementʳ _) ⟨ ∨-cong ⟩
                                      (∧-congˡ $ ∧-complementʳ _) ⟩
    (y ∧ ⊥) ∨ (x ∧ ⊥)              ≈⟨ ∧-zeroʳ _ ⟨ ∨-cong ⟩ ∧-zeroʳ _ ⟩
    ⊥ ∨ ⊥                          ≈⟨ ∨-identityʳ _ ⟩
    ⊥                              ∎

  lem₃ = begin
    (x ∧ y) ∨ ¬ x          ≈⟨ ∨-∧-distribʳ _ _ _ ⟩
    (x ∨ ¬ x) ∧ (y ∨ ¬ x)  ≈⟨ ∧-congʳ $ ∨-complementʳ _ ⟩
    ⊤ ∧ (y ∨ ¬ x)          ≈⟨ ∧-identityˡ _ ⟩
    y ∨ ¬ x                ≈⟨ ∨-comm _ _ ⟩
    ¬ x ∨ y                ∎

  lem₂ = begin
    (x ∧ y) ∨ (¬ x ∨ ¬ y)  ≈˘⟨ ∨-assoc _ _ _ ⟩
    ((x ∧ y) ∨ ¬ x) ∨ ¬ y  ≈⟨ ∨-congʳ lem₃ ⟩
    (¬ x ∨ y) ∨ ¬ y        ≈⟨ ∨-assoc _ _ _ ⟩
    ¬ x ∨ (y ∨ ¬ y)        ≈⟨ ∨-congˡ $ ∨-complementʳ _ ⟩
    ¬ x ∨ ⊤                ≈⟨ ∨-zeroʳ _ ⟩
    ⊤                      ∎

deMorgan₂ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y
deMorgan₂ x y = begin
  ¬ (x ∨ y)          ≈˘⟨ ¬-cong $ ((¬-involutive _) ⟨ ∨-cong ⟩ (¬-involutive _)) ⟩
  ¬ (¬ ¬ x ∨ ¬ ¬ y)  ≈˘⟨ ¬-cong $ deMorgan₁ _ _ ⟩
  ¬ ¬ (¬ x ∧ ¬ y)    ≈⟨ ¬-involutive _ ⟩
  ¬ x ∧ ¬ y          ∎

-- One can replace the underlying equality with an equivalent one.

replace-equality :
  {_≈′_ : Rel Carrier b₂} →
  (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → BooleanAlgebra _ _
replace-equality {_≈′_} ≈⇔≈′ = record
  { _≈_              = _≈′_
  ; _∨_              = _∨_
  ; _∧_              = _∧_
  ; ¬_               = ¬_
  ; ⊤                = ⊤
  ; ⊥                = ⊥
  ; isBooleanAlgebra =  record
    { isDistributiveLattice = DistributiveLattice.isDistributiveLattice
                                (DL.replace-equality ≈⇔≈′)
    ; ∨-complementʳ         = λ x → to ⟨$⟩ ∨-complementʳ x
    ; ∧-complementʳ         = λ x → to ⟨$⟩ ∧-complementʳ x
    ; ¬-cong                = λ i≈j → to ⟨$⟩ ¬-cong (from ⟨$⟩ i≈j)
    }
  } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})

------------------------------------------------------------------------
-- (⊕, ∧, id, ⊥, ⊤) is a commutative ring

-- This construction is parameterised over the definition of xor.

module XorRing
  (xor : Op₂ Carrier)
  (⊕-def : ∀ x y → xor x y ≈ (x ∨ y) ∧ ¬ (x ∧ y))
  where

  private
    infixl 6 _⊕_

    _⊕_ : Op₂ Carrier
    _⊕_ = xor

    helper : ∀ {x y u v} → x ≈ y → u ≈ v → x ∧ ¬ u ≈ y ∧ ¬ v
    helper x≈y u≈v = x≈y ⟨ ∧-cong ⟩ ¬-cong u≈v

  ⊕-cong : Congruent₂ _⊕_
  ⊕-cong {x} {y} {u} {v} x≈y u≈v = begin
    x ⊕ u                ≈⟨ ⊕-def _ _ ⟩
    (x ∨ u) ∧ ¬ (x ∧ u)  ≈⟨ helper (x≈y ⟨ ∨-cong ⟩ u≈v)
                                   (x≈y ⟨ ∧-cong ⟩ u≈v) ⟩
    (y ∨ v) ∧ ¬ (y ∧ v)  ≈˘⟨ ⊕-def _ _ ⟩
    y ⊕ v                ∎

  ⊕-comm : Commutative _⊕_
  ⊕-comm x y = begin
    x ⊕ y                ≈⟨ ⊕-def _ _ ⟩
    (x ∨ y) ∧ ¬ (x ∧ y)  ≈⟨ helper (∨-comm _ _) (∧-comm _ _) ⟩
    (y ∨ x) ∧ ¬ (y ∧ x)  ≈˘⟨ ⊕-def _ _ ⟩
    y ⊕ x                ∎

  ⊕-¬-distribˡ : ∀ x y → ¬ (x ⊕ y) ≈ ¬ x ⊕ y
  ⊕-¬-distribˡ x y = begin
    ¬ (x ⊕ y)                              ≈⟨ ¬-cong $ ⊕-def _ _ ⟩
    ¬ ((x ∨ y) ∧ (¬ (x ∧ y)))              ≈⟨ ¬-cong (∧-∨-distribʳ _ _ _) ⟩
    ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y)))  ≈⟨ ¬-cong $ ∨-congˡ $ ∧-congˡ $ ¬-cong (∧-comm _ _) ⟩
    ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x)))  ≈⟨ ¬-cong $ lem _ _ ⟨ ∨-cong ⟩ lem _ _ ⟩
    ¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x))              ≈⟨ deMorgan₂ _ _ ⟩
    ¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x)              ≈⟨ ∧-congʳ $ deMorgan₁ _ _ ⟩
    (¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x)          ≈⟨ helper (∨-congˡ $ ¬-involutive _) (∧-comm _ _) ⟩
    (¬ x ∨ y) ∧ ¬ (¬ x ∧ y)                ≈˘⟨ ⊕-def _ _ ⟩
    ¬ x ⊕ y                                ∎
    where
    lem : ∀ x y → x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y
    lem x y = begin
      x ∧ ¬ (x ∧ y)          ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩
      x ∧ (¬ x ∨ ¬ y)        ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
      (x ∧ ¬ x) ∨ (x ∧ ¬ y)  ≈⟨ ∨-congʳ $ ∧-complementʳ _ ⟩
      ⊥ ∨ (x ∧ ¬ y)          ≈⟨ ∨-identityˡ _ ⟩
      x ∧ ¬ y                ∎

  ⊕-¬-distribʳ : ∀ x y → ¬ (x ⊕ y) ≈ x ⊕ ¬ y
  ⊕-¬-distribʳ x y = begin
    ¬ (x ⊕ y)  ≈⟨ ¬-cong $ ⊕-comm _ _ ⟩
    ¬ (y ⊕ x)  ≈⟨ ⊕-¬-distribˡ _ _ ⟩
    ¬ y ⊕ x    ≈⟨ ⊕-comm _ _ ⟩
    x ⊕ ¬ y    ∎

  ⊕-annihilates-¬ : ∀ x y → x ⊕ y ≈ ¬ x ⊕ ¬ y
  ⊕-annihilates-¬ x y = begin
    x ⊕ y        ≈˘⟨ ¬-involutive _ ⟩
    ¬ ¬ (x ⊕ y)  ≈⟨ ¬-cong $ ⊕-¬-distribˡ _ _ ⟩
    ¬ (¬ x ⊕ y)  ≈⟨ ⊕-¬-distribʳ _ _ ⟩
    ¬ x ⊕ ¬ y    ∎

  ⊕-identityˡ : LeftIdentity ⊥ _⊕_
  ⊕-identityˡ x = begin
    ⊥ ⊕ x                ≈⟨ ⊕-def _ _ ⟩
    (⊥ ∨ x) ∧ ¬ (⊥ ∧ x)  ≈⟨ helper (∨-identityˡ _) (∧-zeroˡ _) ⟩
    x ∧ ¬ ⊥              ≈⟨ ∧-congˡ ¬⊥=⊤ ⟩
    x ∧ ⊤                ≈⟨ ∧-identityʳ _ ⟩
    x                    ∎

  ⊕-identityʳ : RightIdentity ⊥ _⊕_
  ⊕-identityʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-identityˡ _

  ⊕-identity : Identity ⊥ _⊕_
  ⊕-identity = ⊕-identityˡ , ⊕-identityʳ

  ⊕-inverseˡ : LeftInverse ⊥ id _⊕_
  ⊕-inverseˡ x = begin
    x ⊕ x               ≈⟨ ⊕-def _ _ ⟩
    (x ∨ x) ∧ ¬ (x ∧ x) ≈⟨ helper (∨-idempotent _) (∧-idempotent _) ⟩
    x ∧ ¬ x             ≈⟨ ∧-complementʳ _ ⟩
    ⊥                   ∎

  ⊕-inverseʳ : RightInverse ⊥ id _⊕_
  ⊕-inverseʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-inverseˡ _

  ⊕-inverse : Inverse ⊥ id _⊕_
  ⊕-inverse = ⊕-inverseˡ , ⊕-inverseʳ

  ∧-distribˡ-⊕ : _∧_ DistributesOverˡ _⊕_
  ∧-distribˡ-⊕ x y z = begin
    x ∧ (y ⊕ z)                ≈⟨ ∧-congˡ $ ⊕-def _ _ ⟩
    x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈˘⟨ ∧-assoc _ _ _ ⟩
    (x ∧ (y ∨ z)) ∧ ¬ (y ∧ z)  ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩
    (x ∧ (y ∨ z)) ∧
    (¬ y ∨ ¬ z)                ≈˘⟨ ∨-identityˡ _ ⟩
    ⊥ ∨
    ((x ∧ (y ∨ z)) ∧
    (¬ y ∨ ¬ z))               ≈⟨ ∨-congʳ lem₃ ⟩
    ((x ∧ (y ∨ z)) ∧ ¬ x) ∨
    ((x ∧ (y ∨ z)) ∧
    (¬ y ∨ ¬ z))               ≈˘⟨ ∧-∨-distribˡ _ _ _ ⟩
    (x ∧ (y ∨ z)) ∧
    (¬ x ∨ (¬ y ∨ ¬ z))        ≈˘⟨ ∧-congˡ $ ∨-congˡ (deMorgan₁ _ _) ⟩
    (x ∧ (y ∨ z)) ∧
    (¬ x ∨ ¬ (y ∧ z))          ≈˘⟨ ∧-congˡ (deMorgan₁ _ _) ⟩
    (x ∧ (y ∨ z)) ∧
    ¬ (x ∧ (y ∧ z))            ≈⟨ helper refl lem₁ ⟩
    (x ∧ (y ∨ z)) ∧
    ¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ ∧-congʳ $ ∧-∨-distribˡ _ _ _ ⟩
    ((x ∧ y) ∨ (x ∧ z)) ∧
    ¬ ((x ∧ y) ∧ (x ∧ z))      ≈˘⟨ ⊕-def _ _ ⟩
    (x ∧ y) ⊕ (x ∧ z)          ∎
      where
      lem₂ = begin
        x ∧ (y ∧ z)  ≈˘⟨ ∧-assoc _ _ _ ⟩
        (x ∧ y) ∧ z  ≈⟨ ∧-congʳ $ ∧-comm _ _ ⟩
        (y ∧ x) ∧ z  ≈⟨ ∧-assoc _ _ _ ⟩
        y ∧ (x ∧ z)  ∎

      lem₁ = begin
        x ∧ (y ∧ z)        ≈˘⟨ ∧-congʳ (∧-idempotent _) ⟩
        (x ∧ x) ∧ (y ∧ z)  ≈⟨ ∧-assoc _ _ _ ⟩
        x ∧ (x ∧ (y ∧ z))  ≈⟨ ∧-congˡ lem₂ ⟩
        x ∧ (y ∧ (x ∧ z))  ≈˘⟨ ∧-assoc _ _ _ ⟩
        (x ∧ y) ∧ (x ∧ z)  ∎

      lem₃ = begin
        ⊥                      ≈˘⟨ ∧-zeroʳ _ ⟩
        (y ∨ z) ∧ ⊥            ≈˘⟨ ∧-congˡ (∧-complementʳ _) ⟩
        (y ∨ z) ∧ (x ∧ ¬ x)    ≈˘⟨ ∧-assoc _ _ _ ⟩
        ((y ∨ z) ∧ x) ∧ ¬ x    ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl  ⟩
        (x ∧ (y ∨ z)) ∧ ¬ x    ∎

  ∧-distribʳ-⊕ : _∧_ DistributesOverʳ _⊕_
  ∧-distribʳ-⊕ = comm+distrˡ⇒distrʳ ⊕-cong ∧-comm ∧-distribˡ-⊕

  ∧-distrib-⊕ : _∧_ DistributesOver _⊕_
  ∧-distrib-⊕ = ∧-distribˡ-⊕ , ∧-distribʳ-⊕

  private

    lemma₂ : ∀ x y u v →
             (x ∧ y) ∨ (u ∧ v) ≈
             ((x ∨ u) ∧ (y ∨ u)) ∧
             ((x ∨ v) ∧ (y ∨ v))
    lemma₂ x y u v = begin
        (x ∧ y) ∨ (u ∧ v)              ≈⟨ ∨-∧-distribˡ _ _ _ ⟩
        ((x ∧ y) ∨ u) ∧ ((x ∧ y) ∨ v)  ≈⟨ ∨-∧-distribʳ _ _ _
                                            ⟨ ∧-cong ⟩
                                          ∨-∧-distribʳ _ _ _ ⟩
        ((x ∨ u) ∧ (y ∨ u)) ∧
        ((x ∨ v) ∧ (y ∨ v))            ∎

  ⊕-assoc : Associative _⊕_
  ⊕-assoc x y z = sym $ begin
    x ⊕ (y ⊕ z)                                ≈⟨ refl ⟨ ⊕-cong ⟩ ⊕-def _ _ ⟩
    x ⊕ ((y ∨ z) ∧ ¬ (y ∧ z))                  ≈⟨ ⊕-def _ _ ⟩
      (x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))) ∧
    ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))              ≈⟨ lem₃ ⟨ ∧-cong ⟩ lem₄ ⟩
    (((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
    (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ ∧-assoc _ _ _ ⟩
    ((x ∨ y) ∨ z) ∧
    (((x ∨ ¬ y) ∨ ¬ z) ∧
     (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈⟨ ∧-congˡ lem₅ ⟩
    ((x ∨ y) ∨ z) ∧
    (((¬ x ∨ ¬ y) ∨ z) ∧
     (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈˘⟨ ∧-assoc _ _ _ ⟩
    (((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
    (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ lem₁ ⟨ ∧-cong ⟩ lem₂ ⟩
      (((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z) ∧
    ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)              ≈˘⟨ ⊕-def _ _ ⟩
    ((x ∨ y) ∧ ¬ (x ∧ y)) ⊕ z                  ≈˘⟨ ⊕-def _ _ ⟨ ⊕-cong ⟩ refl ⟩
    (x ⊕ y) ⊕ z                                ∎
    where
    lem₁ = begin
      ((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)  ≈˘⟨ ∨-∧-distribʳ _ _ _ ⟩
      ((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z        ≈˘⟨ ∨-congʳ $ ∧-congˡ (deMorgan₁ _ _) ⟩
      ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z          ∎

    lem₂' = begin
      (x ∨ ¬ y) ∧ (¬ x ∨ y)              ≈˘⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩
      (⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤)  ≈˘⟨  (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _)
                                                ⟨ ∧-cong ⟩
                                              (∧-congˡ $ ∨-complementˡ _) ⟩
      ((¬ x ∨ x) ∧ (¬ y ∨ x)) ∧
      ((¬ x ∨ y) ∧ (¬ y ∨ y))            ≈˘⟨ lemma₂ _ _ _ _ ⟩
      (¬ x ∧ ¬ y) ∨ (x ∧ y)              ≈˘⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
      ¬ (x ∨ y) ∨ ¬ ¬ (x ∧ y)            ≈˘⟨ deMorgan₁ _ _ ⟩
      ¬ ((x ∨ y) ∧ ¬ (x ∧ y))            ∎

    lem₂ = begin
      ((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)  ≈˘⟨ ∨-∧-distribʳ _ _ _ ⟩
      ((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z          ≈⟨ ∨-congʳ lem₂' ⟩
      ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z          ≈˘⟨ deMorgan₁ _ _ ⟩
      ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)          ∎

    lem₃ = begin
      x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))          ≈⟨ ∨-congˡ $ ∧-congˡ $ deMorgan₁ _ _ ⟩
      x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z))        ≈⟨ ∨-∧-distribˡ _ _ _ ⟩
      (x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z))  ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩
      ((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)  ∎

    lem₄' = begin
      ¬ ((y ∨ z) ∧ ¬ (y ∧ z))    ≈⟨ deMorgan₁ _ _ ⟩
      ¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z)    ≈⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
      (¬ y ∧ ¬ z) ∨ (y ∧ z)      ≈⟨ lemma₂ _ _ _ _ ⟩
      ((¬ y ∨ y) ∧ (¬ z ∨ y)) ∧
      ((¬ y ∨ z) ∧ (¬ z ∨ z))    ≈⟨ (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _)
                                      ⟨ ∧-cong ⟩
                                   (∧-congˡ $ ∨-complementˡ _) ⟩
      (⊤ ∧ (y ∨ ¬ z)) ∧
      ((¬ y ∨ z) ∧ ⊤)            ≈⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩
      (y ∨ ¬ z) ∧ (¬ y ∨ z)      ∎

    lem₄ = begin
      ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))  ≈⟨ deMorgan₁ _ _ ⟩
      ¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ ∨-congˡ lem₄' ⟩
      ¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z))  ≈⟨ ∨-∧-distribˡ _ _ _ ⟩
      (¬ x ∨ (y     ∨ ¬ z)) ∧
      (¬ x ∨ (¬ y ∨ z))              ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩
      ((¬ x ∨ y)     ∨ ¬ z) ∧
      ((¬ x ∨ ¬ y) ∨ z)              ≈⟨ ∧-comm _ _ ⟩
      ((¬ x ∨ ¬ y) ∨ z) ∧
      ((¬ x ∨ y)     ∨ ¬ z)          ∎

    lem₅ = begin
      ((x ∨ ¬ y) ∨ ¬ z) ∧
      (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈˘⟨ ∧-assoc _ _ _ ⟩
      (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
      ((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-congʳ $ ∧-comm _ _ ⟩
      (((¬ x ∨ ¬ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
      ((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-assoc _ _ _ ⟩
      ((¬ x ∨ ¬ y) ∨ z) ∧
      (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ∎

  ⊕-isMagma : IsMagma _⊕_
  ⊕-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = ⊕-cong
    }

  ⊕-isSemigroup : IsSemigroup _⊕_
  ⊕-isSemigroup = record
    { isMagma = ⊕-isMagma
    ; assoc   = ⊕-assoc
    }

  ⊕-⊥-isMonoid : IsMonoid _⊕_ ⊥
  ⊕-⊥-isMonoid = record
    { isSemigroup = ⊕-isSemigroup
    ; identity    = ⊕-identity
    }

  ⊕-⊥-isGroup : IsGroup _⊕_ ⊥ id
  ⊕-⊥-isGroup = record
    { isMonoid = ⊕-⊥-isMonoid
    ; inverse  = ⊕-inverse
    ; ⁻¹-cong  = id
    }

  ⊕-⊥-isAbelianGroup : IsAbelianGroup _⊕_ ⊥ id
  ⊕-⊥-isAbelianGroup = record
    { isGroup = ⊕-⊥-isGroup
    ; comm    = ⊕-comm
    }

  ⊕-∧-isRing : IsRing _⊕_ _∧_ id ⊥ ⊤
  ⊕-∧-isRing = record
    { +-isAbelianGroup = ⊕-⊥-isAbelianGroup
    ; *-isMonoid = ∧-⊤-isMonoid
    ; distrib = ∧-distrib-⊕
    }

  isCommutativeRing : IsCommutativeRing _⊕_ _∧_ id ⊥ ⊤
  isCommutativeRing = record
    { isRing = ⊕-∧-isRing
    ; *-comm = ∧-comm
    }

  commutativeRing : CommutativeRing _ _
  commutativeRing = record
    { _+_               = _⊕_
    ; _*_               = _∧_
    ; -_                = id
    ; 0#                = ⊥
    ; 1#                = ⊤
    ; isCommutativeRing = isCommutativeRing
    }

infixl 6 _⊕_

_⊕_ : Op₂ Carrier
x ⊕ y = (x ∨ y) ∧ ¬ (x ∧ y)

module DefaultXorRing = XorRing _⊕_ (λ _ _ → refl)


text:
-- Andreas, 2017-08-13, issue #2684
-- Better error for abstract constructor.

abstract
  data D : Set where
    c : D

  data E : Set where
    c : E

test : D
test = c

-- Expected:
-- Constructor c is abstract, thus, not in scope here
-- when checking that the expression c has type D

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Check that unquoted functions are termination checked.
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality

`⊥ : Type
`⊥ = def (quote ⊥) []

⊥-elim : ∀ {a} {A : Set a} → ⊥ → A
⊥-elim ()

{-
Generate
  cheat : ⊥
  cheat = cheat
-}
makeLoop : TC Term
makeLoop =
  freshName "cheat" >>= λ cheat →
  declareDef (vArg cheat) `⊥ >>= λ _ →
  defineFun cheat (clause [] (def cheat []) ∷ []) >>= λ _ →
  returnTC (def cheat [])

macro
  magic : Tactic
  magic hole =
    makeLoop >>= λ loop →
    unify hole (def (quote ⊥-elim) (vArg loop ∷ []))

postulate
  ComplexityClass : Set
  P NP : ComplexityClass

thm : P ≡ NP → ⊥
thm = magic

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue1290b where

open import Issue1290

data Eq (x : R) : R → Set where
  refl : Eq x x

test : Eq x (exp x)
test = refl


text:
------------------------------------------------------------------------
-- Simple combinators working solely on and with functions
------------------------------------------------------------------------

module Data.Function where

infixr 9 _∘_ _∘′_ _∘₀_ _∘₁_
infixl 1 _on_ _on₁_
infixl 1 _⟨_⟩_ _⟨_⟩₁_
infixr 0 _-[_]₁-_ _-[_]-_ _$_
infix  0 _∶_ _∶₁_

------------------------------------------------------------------------
-- Types

-- Unary functions on a given set.

Fun₁ : Set → Set
Fun₁ a = a → a

-- Binary functions on a given set.

Fun₂ : Set → Set
Fun₂ a = a → a → a

------------------------------------------------------------------------
-- Functions

_∘_ : {A : Set} {B : A → Set} {C : {x : A} → B x → Set} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

_∘′_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
f ∘′ g = _∘_ f g

_∘₀_ : {A : Set} {B : A → Set} {C : {x : A} → B x → Set₁} →
       (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
       ((x : A) → C (g x))
f ∘₀ g = λ x → f (g x)

_∘₁_ : {A : Set₁} {B : A → Set₁} {C : {x : A} → B x → Set₁} →
       (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
       ((x : A) → C (g x))
f ∘₁ g = λ x → f (g x)

id : {a : Set} → a → a
id x = x

id₁ : {a : Set₁} → a → a
id₁ x = x

const : {a b : Set} → a → b → a
const x = λ _ → x

const₁ : {a : Set₁} {b : Set} → a → b → a
const₁ x = λ _ → x

flip : {A B : Set} {C : A → B → Set} →
       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ x y → f y x

flip₁ : {A B : Set} {C : A → B → Set₁} →
        ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip₁ f = λ x y → f y x

-- Note that _$_ is right associative, like in Haskell. If you want a
-- left associative infix application operator, use
-- Category.Functor._<$>_, available from
-- Category.Monad.Identity.IdentityMonad.

_$_ : {a : Set} {b : a → Set} → ((x : a) → b x) → ((x : a) → b x)
f $ x = f x

_⟨_⟩_ : {a b c : Set} → a → (a → b → c) → b → c
x ⟨ f ⟩ y = f x y

_⟨_⟩₁_ : {a b : Set} → a → (a → b → Set) → b → Set
x ⟨ f ⟩₁ y = f x y

_on_ : {a b c : Set} → (b → b → c) → (a → b) → (a → a → c)
_*_ on f = λ x y → f x * f y

_on₁_ : {a b : Set} {c : Set₁} → (b → b → c) → (a → b) → (a → a → c)
_*_ on₁ f = λ x y → f x * f y

_-[_]-_ : {a b c d e : Set} →
          (a → b → c) → (c → d → e) → (a → b → d) → (a → b → e)
f -[ _*_ ]- g = λ x y → f x y * g x y

_-[_]₁-_ : {a b : Set} →
           (a → b → Set) → (Set → Set → Set) → (a → b → Set) →
           (a → b → Set)
f -[ _*_ ]₁- g = λ x y → f x y * g x y

-- In Agda you cannot annotate every subexpression with a type
-- signature. This function can be used instead.
--
-- You should think of the colon as being mirrored around its vertical
-- axis; the type comes first.

_∶_ : (A : Set) → A → A
_ ∶ x = x

_∶₁_ : (A : Set₁) → A → A
_ ∶₁ x = x

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --safe #-}

module Definition.Typed.Consequences.Injectivity where

open import Definition.Untyped hiding (wk)
import Definition.Untyped as U
open import Definition.Untyped.Properties

open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Fundamental.Reducibility

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Helper function of injectivity for specific reducible Π-types
injectivity′ : ∀ {F G H E rF lF rH lH  rΠ lG lE Γ lΠ l}
               ([ΠFG] : Γ ⊩⟨ l ⟩Π Π F ^ rF ° lF  ▹ G ° lG ° lΠ ^[ rΠ , lΠ ] )
             → Γ ⊩⟨ l ⟩ Π F ^ rF ° lF ▹ G ° lG  ° lΠ ≡ Π H ^ rH ° lH  ▹ E ° lE  ° lΠ ^ [ rΠ , ι lΠ ] / Π-intr [ΠFG]
             → Γ ⊢ F ≡ H ^ [ rF , ι lF ]
             × rF PE.≡ rH
             × lF PE.≡ lH
             × lG PE.≡ lE
             × Γ ∙ F ^ [ rF , ι lF ] ⊢ G ≡ E ^ [ rΠ , ι  lG ]
injectivity′ {F₁} {G₁} {H} {E} {lF = lF₁} {rΠ = rΠ} {Γ = Γ}
         (noemb (Πᵣ ! lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext))
         (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let F≡F₁ , rF≡rF₁ , lF≡lF₁ , G≡G₁ , lG≡lG₁ , _ = Π-PE-injectivity (whnfRed* (red D) Πₙ)
      H≡F′ , rH≡rF′ , lH≡lF′ , E≡G′ , lE≡lG′ , _ = Π-PE-injectivity (whnfRed* D′ Πₙ)
      ⊢Γ = wf ⊢F
      [F]₁ = [F] id ⊢Γ
      [F]′ = irrelevance′ (PE.trans (wk-id _) (PE.sym F≡F₁)) [F]₁
      [x∷F] = neuTerm ([F] (step id) (⊢Γ ∙ ⊢F)) (var 0) (var (⊢Γ ∙ ⊢F) here)
                      (refl (var (⊢Γ ∙ ⊢F) here))
      [G]₁ = [G] (step id) (⊢Γ ∙ ⊢F) [x∷F]
      [G]′ = PE.subst₂ (λ x y → _ ∙ y ^ _ ⊩⟨ _ ⟩ x ^ _)
                       (PE.trans (wkSingleSubstId _) (PE.sym G≡G₁))
                       (PE.sym F≡F₁) [G]₁
      [F≡H]₁ = [F≡F′] id ⊢Γ
      [F≡H]′ = irrelevanceEq″ (PE.trans (wk-id _) (PE.sym F≡F₁))
                              (PE.trans (wk-id _) (PE.sym H≡F′))
                              PE.refl PE.refl
                              [F]₁ [F]′ [F≡H]₁
      [G≡E]₁ = [G≡G′] (step id) (⊢Γ ∙ ⊢F) [x∷F]
      [G≡E]′ = irrelevanceEqLift″ (PE.trans (wkSingleSubstId _) (PE.sym G≡G₁))
                                   (PE.trans (wkSingleSubstId _) (PE.sym E≡G′))
                                   (PE.sym F≡F₁) [G]₁ [G]′ [G≡E]₁
  in  PE.subst (λ r → Γ ⊢ _ ≡ _ ^ [ r , ι lF₁ ] ) (PE.sym rF≡rF₁)
        (PE.subst (λ l → Γ ⊢ F₁ ≡ H ^ [ ! , l ] ) (PE.cong ι (PE.sym lF≡lF₁))
          (escapeEq [F]′ [F≡H]′)) ,
     ( PE.trans rF≡rF₁ (PE.sym rH≡rF′) ,
     ( PE.trans lF≡lF₁ (PE.sym lH≡lF′) ,
     ( PE.trans lG≡lG₁ (PE.sym lE≡lG′) ,
        PE.subst (λ r → (_ ∙ _ ^ [ r , _ ] ) ⊢ _ ≡ _ ^ _) (PE.sym rF≡rF₁)
         (PE.subst (λ l → (Γ ∙ F₁  ^ [ ! , ι lF₁ ] ) ⊢ G₁ ≡ E ^ [ rΠ , l ]) (PE.cong ι  (PE.sym lG≡lG₁))
          (PE.subst (λ l → (Γ ∙ F₁ ^ [ ! , l ] ) ⊢ G₁ ≡ E ^  [ rΠ , ι lG ]) (PE.cong ι (PE.sym lF≡lF₁))
           (escapeEq [G]′ [G≡E]′))))))

injectivity′ {F₁} {G₁} {H} {E} {lF = lF₁} {rΠ = rΠ} {Γ = Γ}
         (noemb (Πᵣ % lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext))
         (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let F≡F₁ , rF≡rF₁ , lF≡lF₁ , G≡G₁ , lG≡lG₁ , _ = Π-PE-injectivity (whnfRed* (red D) Πₙ)
      H≡F′ , rH≡rF′ , lH≡lF′ , E≡G′ , lE≡lG′ , _ = Π-PE-injectivity (whnfRed* D′ Πₙ)
      ⊢Γ = wf ⊢F
      [F]₁ = [F] id ⊢Γ
      [F]′ = irrelevance′ (PE.trans (wk-id _) (PE.sym F≡F₁)) [F]₁
      [x∷F] = neuTerm ([F] (step id) (⊢Γ ∙ ⊢F)) (var 0) (var (⊢Γ ∙ ⊢F) here)
                      (proof-irrelevance (var (⊢Γ ∙ ⊢F) here) (var (⊢Γ ∙ ⊢F) here))
      [G]₁ = [G] (step id) (⊢Γ ∙ ⊢F) [x∷F]
      [G]′ = PE.subst₂ (λ x y → _ ∙ y ^ _ ⊩⟨ _ ⟩ x ^ _)
                       (PE.trans (wkSingleSubstId _) (PE.sym G≡G₁))
                       (PE.sym F≡F₁) [G]₁
      [F≡H]₁ = [F≡F′] id ⊢Γ
      [F≡H]₁ = [F≡F′] id ⊢Γ
      [F≡H]′ = irrelevanceEq″ (PE.trans (wk-id _) (PE.sym F≡F₁))
                              (PE.trans (wk-id _) (PE.sym H≡F′))
                              PE.refl PE.refl
                              [F]₁ [F]′ [F≡H]₁
      [G≡E]₁ = [G≡G′] (step id) (⊢Γ ∙ ⊢F) [x∷F]
      [G≡E]′ = irrelevanceEqLift″ (PE.trans (wkSingleSubstId _) (PE.sym G≡G₁))
                                   (PE.trans (wkSingleSubstId _) (PE.sym E≡G′))
                                   (PE.sym F≡F₁) [G]₁ [G]′ [G≡E]₁
  in  PE.subst (λ r → Γ ⊢ _ ≡ _ ^ [ r , ι lF₁ ] ) (PE.sym rF≡rF₁)
        (PE.subst (λ l → Γ ⊢ F₁ ≡ H ^ [ % , l ] ) (PE.cong ι (PE.sym lF≡lF₁))
          (escapeEq [F]′ [F≡H]′)) ,
     ( PE.trans rF≡rF₁ (PE.sym rH≡rF′) ,
     ( PE.trans lF≡lF₁ (PE.sym lH≡lF′) ,
     ( PE.trans lG≡lG₁ (PE.sym lE≡lG′) ,
        PE.subst (λ r → (_ ∙ _ ^ [ r , _ ] ) ⊢ _ ≡ _ ^ _) (PE.sym rF≡rF₁)
         (PE.subst (λ l → (Γ ∙ F₁  ^ [ % , ι lF₁ ] ) ⊢ G₁ ≡ E ^ [ rΠ , l ]) (PE.cong ι  (PE.sym lG≡lG₁))
          (PE.subst (λ l → (Γ ∙ F₁ ^ [ % , l ] ) ⊢ G₁ ≡ E ^  [ rΠ , ι lG ]) (PE.cong ι (PE.sym lF≡lF₁))
           (escapeEq [G]′ [G≡E]′))))))

injectivity′ (emb emb< x) [ΠFG≡ΠHE] = injectivity′ x [ΠFG≡ΠHE]
injectivity′ (emb ∞< x) [ΠFG≡ΠHE] = injectivity′ x [ΠFG≡ΠHE]

-- Injectivity of Π
injectivity : ∀ {Γ F G H E rF lF lH lG lE rH rΠ lΠ} →
              Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ≡ Π H ^ rH ° lH ▹ E ° lE ° lΠ ^ [ rΠ , ι lΠ ]
            → Γ ⊢ F ≡ H ^ [ rF , ι lF ]
            × rF PE.≡ rH
            × lF PE.≡ lH
            × lG PE.≡ lE
            × Γ ∙ F ^ [ rF , ι lF ] ⊢ G ≡ E ^ [ rΠ , ι lG ]
injectivity ⊢ΠFG≡ΠHE =
  let [ΠFG] , _ , [ΠFG≡ΠHE] = reducibleEq ⊢ΠFG≡ΠHE
  in  injectivity′ (Π-elim [ΠFG])
                   (irrelevanceEq [ΠFG] (Π-intr (Π-elim [ΠFG])) [ΠFG≡ΠHE])

Uinjectivity′ : ∀ {Γ r₁ r₂ l₁ l₂ lU l}
               ([U] : Γ ⊩⟨ l ⟩U Univ r₁ l₁ ^ lU)
             → Γ ⊩⟨ l ⟩ Univ r₁ l₁ ≡ Univ r₂ l₂ ^ [ ! , lU ] / U-intr [U]
             → r₁ PE.≡ r₂ × l₁ PE.≡ l₂
Uinjectivity′ (noemb (Uᵣ r l′ l< eq d)) D =
  let A , B = Univ-PE-injectivity (whnfRed* D Uₙ)
      A' , B' = Univ-PE-injectivity (whnfRed* (red d) Uₙ)
  in (PE.trans A' (PE.sym A)) , (PE.trans B' (PE.sym B))
Uinjectivity′ (emb emb< a) b = Uinjectivity′ a b
Uinjectivity′ (emb ∞< a) b = Uinjectivity′ a b

Uinjectivity : ∀ {Γ r₁ r₂ l₁ l₂ lU} →
                 Γ ⊢ Univ r₁ l₁ ≡ Univ r₂ l₂  ^ [ ! , lU ] →
                 r₁ PE.≡ r₂ × l₁ PE.≡ l₂
Uinjectivity ⊢U≡U =
  let [U] , _ , [U≡U] = reducibleEq ⊢U≡U
  in Uinjectivity′ (U-elim [U]) (irrelevanceEq [U] (U-intr (U-elim [U])) [U≡U])

-- injectivity of ∃

∃injectivity′ : ∀ {F G H E Γ l∃ l}
               ([∃FG] : Γ ⊩⟨ l ⟩∃ ∃ F ▹ G ^ l∃ )
             → Γ ⊩⟨ l ⟩ ∃ F ▹ G ≡ ∃ H ▹ E ^ [ % , ι l∃ ] / ∃-intr [∃FG]
             → Γ ⊢ F ≡ H ^ [ % , ι l∃ ]
             × Γ ∙ F ^ [ % , ι l∃ ] ⊢ G ≡ E ^ [ % , ι l∃ ]
∃injectivity′ {F₁} {G₁} {H} {E} {Γ = Γ}
         (noemb (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext))
         (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  let F≡F₁ , G≡G₁ = ∃-PE-injectivity (whnfRed* (red D) ∃ₙ)
      H≡F′ , E≡G′ = ∃-PE-injectivity (whnfRed* D′ ∃ₙ)
      ⊢Γ = wf ⊢F
      [F]₁ = [F] id ⊢Γ
      [F]′ = irrelevance′ (PE.trans (wk-id _) (PE.sym F≡F₁)) [F]₁
      [x∷F] = neuTerm ([F] (step id) (⊢Γ ∙ ⊢F)) (var 0) (var (⊢Γ ∙ ⊢F) here) (proof-irrelevance (var (⊢Γ ∙ ⊢F) here) (var (⊢Γ ∙ ⊢F) here))
      [G]₁ = [G] (step id) (⊢Γ ∙ ⊢F) [x∷F]
      [G]′ = PE.subst₂ (λ x y → _ ∙ y ^ _ ⊩⟨ _ ⟩ x ^ _)
                       (PE.trans (wkSingleSubstId _) (PE.sym G≡G₁))
                       (PE.sym F≡F₁) [G]₁
      [F≡H]₁ = [F≡F′] id ⊢Γ
      [F≡H]′ = irrelevanceEq″ (PE.trans (wk-id _) (PE.sym F≡F₁))
                              (PE.trans (wk-id _) (PE.sym H≡F′))
                              PE.refl PE.refl
                              [F]₁ [F]′ [F≡H]₁
      [G≡E]₁ = [G≡G′] (step id) (⊢Γ ∙ ⊢F) [x∷F]
      [G≡E]′ = irrelevanceEqLift″ (PE.trans (wkSingleSubstId _) (PE.sym G≡G₁))
                                   (PE.trans (wkSingleSubstId _) (PE.sym E≡G′))
                                   (PE.sym F≡F₁) [G]₁ [G]′ [G≡E]₁
  in escapeEq [F]′ [F≡H]′ , escapeEq [G]′ [G≡E]′
∃injectivity′ (emb emb< x) [∃FG≡∃HE] = ∃injectivity′ x [∃FG≡∃HE]
∃injectivity′ (emb ∞< x) [∃FG≡∃HE] = ∃injectivity′ x [∃FG≡∃HE]

-- Injectivity of ∃
∃injectivity : ∀ {Γ F G H E l∃} →
              Γ ⊢ ∃ F ▹ G ≡ ∃ H ▹ E ^ [ % , ι l∃ ]
            → Γ ⊢ F ≡ H ^ [ % , ι l∃ ]
            × Γ ∙ F ^ [ % , ι l∃ ] ⊢ G ≡ E ^ [ % , ι l∃ ]
∃injectivity ⊢∃FG≡∃HE =
  let [∃FG] , _ , [∃FG≡∃HE] = reducibleEq ⊢∃FG≡∃HE
  in ∃injectivity′ (∃-elim [∃FG])
                   (irrelevanceEq [∃FG] (∃-intr (∃-elim [∃FG])) [∃FG≡∃HE])

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module _ where

import Issue4373.A as A hiding (t)

postulate
  search : ⦃ x : A.T ⦄ → Set

fail : Set
fail = search


text: module Function.Domains.Proofs where

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation.Standard.Relation.Decidable where

open import Light.Variable.Sets
import Light.Implementation.Standard.Data.Empty
import Light.Implementation.Standard.Data.Unit
open import Light.Library.Data.Empty as Empty using (Empty)
open import Light.Library.Data.Unit as Unit using (Unit ; unit)
open import Light.Library.Relation.Decidable using (Library ; Dependencies)

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record
      {
            Implementation ;
            to‐witness = λ ⦃ a ⦄ → Implementation.to‐witness a ;
            to‐false‐witness = λ ⦃ a ⦄ → Implementation.to‐false‐witness a ;
            from‐witness = λ ⦃ a ⦄ → Implementation.from‐witness a ;
            from‐false‐witness = λ ⦃ a ⦄ → Implementation.from‐false‐witness a
      }
      where
      module Implementation where
            open import Relation.Nullary using (yes ; no) renaming (Dec to Decidable) public
            open Relation.Nullary using (does)
            open import Function using (_∘_)
            import Data.Bool as Boolean
            open import Function using (id)
            open import Relation.Nullary.Decidable
                  renaming (
                        toWitness to to‐witness ;
                        fromWitness to from‐witness ;
                        toWitnessFalse to to‐false‐witness ;
                        fromWitnessFalse to from‐false‐witness
                  )
                  public
            open import Light.Implementation.Standard.Relation.Sets using (base) public

            ℓf = id

            if′_then_else_ : Decidable 𝕒 → 𝕓 → 𝕓 → 𝕓
            if′_then_else_ = Boolean.if_then_else_ ∘ does

            if_then_else_ :
                  ∀ (a : Decidable 𝕒)
                  → (∀ ⦃ witness : 𝕒 ⦄ → 𝕓)
                  → (∀ ⦃ witness : 𝕒 → Empty ⦄ → 𝕓)
                  → 𝕓
            if yes w then a else _ = a ⦃ witness = w ⦄
            if no w then _ else a = a ⦃ witness = w ⦄

            module Style where
                  open import Relation.Nullary.Decidable using (True ; False) public
                  open import Relation.Nullary.Negation using () renaming (¬? to ¬_) public
                  open import Relation.Nullary.Product using () renaming (_×-dec_ to _∧_) public
                  open import Relation.Nullary.Sum using () renaming (_⊎-dec_ to _∨_) public
                  open import Relation.Nullary.Implication using () renaming (_→-dec_ to _⇢_) public

                  true : Decidable Unit
                  true = yes unit

                  false : Decidable Empty
                  false = no λ ()

            style = record { Style }

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module _ where

open import Agda.Primitive
open import Agda.Builtin.Equality

data Wrap {a} (A : Set a) : Set a where
  wrap : A → Wrap A

data Unit (A : Set) : Set where
  unit : Unit A

cast : ∀ {A B} → Unit A → Unit B
cast unit = unit

data Functor {a b} (F : Set a → Set b) : Set (lsuc (a ⊔ b)) where
  mkFunctor : (∀ {A B} → (A → B) → F A → F B) → Functor F

fmap : ∀ {a b} {A B : Set a} {F : Set a → Set b} →
            Functor F → (A → B) → F A → F B
fmap (mkFunctor m) = m

FunUnit : Functor Unit
FunUnit = mkFunctor λ _ → cast

postulate
  P : ∀ {a} {A : Set a} → A → Set a
  A : Set

fmapType : ∀ {b} {B : Set} {F : Set → Set b} {x : F A} →
             Functor F → (A → B) → P x → Set _
fmapType {x = x} Fun f _ = P (fmap Fun f x)

postulate
  wrapP : ∀ {a} {A : Set a} (x : A) → P (wrap x)

mutual-block : Set₁

a : Level
a = _

X : Set → Set a
X = _

FunX : Functor X
FunX = mkFunctor _

-- Adds constraint:
--   fmapType FunX wrap (wrapP x) == P (wrap (wrap x))
--   P (fmap FunX wrap (wrap x)   == P (wrap (wrap x))
--   fmap FunX wrap (wrap x)      == wrap (wrap x)
--   ?0 wrap (wrap x)             == wrap (wrap x)
constr₁ : (x : _) → fmapType {x = _} FunX wrap (wrapP x) → P (wrap (wrap x))
constr₁ x p = p

constr₂ : P FunX → P FunUnit
constr₂ p = p

mutual-block = Set


text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT
open import homotopy.Bouquet
open import homotopy.FinWedge
open import homotopy.SphereEndomorphism
open import groups.SphereEndomorphism
open import cw.CW
open import cw.FinCW
open import cw.WedgeOfCells
open import cw.DegreeByProjection {lzero}
open import cohomology.Theory

{- This file should be part of RephraseHigherFinCoboundary,
   but putting these in a separate file seems more effective
   in speeding up type-checking. Could be an Agda bug. -}

module cw.cohomology.cochainequiv.HigherCoboundaryAbstractDefs (OT : OrdinaryTheory lzero)
  {n} (⊙fin-skel : ⊙FinSkeleton (S (S n))) where

open OrdinaryTheory OT
open import cohomology.Bouquet OT

private
  ⊙skel = ⊙FinSkeleton-realize ⊙fin-skel
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel
  skel = ⊙Skeleton.skel ⊙skel
  dec = ⊙FinSkeleton-has-cells-with-dec-eq ⊙fin-skel

  ⊙fin-skel₋₁ = ⊙fcw-init ⊙fin-skel
  ⊙skel₋₁ = ⊙FinSkeleton-realize ⊙fin-skel₋₁
  fin-skel₋₁ = ⊙FinSkeleton.skel ⊙fin-skel₋₁
  I₋₁ = AttachedFinSkeleton.numCells fin-skel₋₁
  skel₋₁ = ⊙Skeleton.skel ⊙skel₋₁
  dec₋₁ = ⊙FinSkeleton-has-cells-with-dec-eq ⊙fin-skel₋₁

open import cw.cohomology.WedgeOfCells OT
open import cw.cohomology.reconstructed.HigherCoboundary OT ⊙skel

⊙function₀ : ⊙FinBouquet I (S (S n)) ⊙→ ⊙Susp (⊙FinBouquet I₋₁ (S n))
⊙function₀ = ⊙Susp-fmap (⊙<– (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ skel₋₁))
          ⊙∘ ⊙cw-∂-before-Susp
          ⊙∘ ⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ skel)

function₁ : Fin I → Fin I₋₁ → Sphere-endo (S n)
function₁ <I <I₋₁ = bwproj Fin-has-dec-eq <I₋₁
                  ∘ <– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁)
                  ∘ cfcod
                  ∘ attaching-last skel <I

abstract
  ⊙function₀' : ⊙FinBouquet I (S (S n)) ⊙→ ⊙Susp (⊙FinBouquet I₋₁ (S n))
  ⊙function₀' = ⊙function₀

  ⊙function₀'-β : ⊙function₀' == ⊙function₀
  ⊙function₀'-β = idp

  function₁' : Fin I → Fin I₋₁ → Sphere-endo (S n)
  function₁' = function₁

  function₁'-β : ∀ <I <I₋₁ → function₁' <I <I₋₁ == function₁ <I <I₋₁
  function₁'-β _ _ = idp

  mega-reduction : ∀ <I <I₋₁ →
      Susp-fmap (fwproj <I₋₁) ∘ fst ⊙function₀' ∘ fwin <I
    ∼ Susp-fmap (function₁' <I <I₋₁)
  mega-reduction <I <I₋₁ = Susp-elim idp idp λ x → ↓-='-in' $ ! $
    ap (Susp-fmap (fwproj <I₋₁) ∘ fst ⊙function₀ ∘ fwin <I) (merid x)
      =⟨ ap-∘
          ( Susp-fmap (fwproj <I₋₁)
          ∘ Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁))
          ∘ cw-∂-before-Susp)
          (Bouquet-to-Xₙ/Xₙ₋₁ skel ∘ fwin <I)
          (merid x) ⟩
    ap ( Susp-fmap (fwproj <I₋₁)
       ∘ Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁))
       ∘ cw-∂-before-Susp)
       (ap (Bouquet-to-Xₙ/Xₙ₋₁ skel ∘ fwin <I) (merid x))
      =⟨ ap (ap ( Susp-fmap (fwproj <I₋₁)
                ∘ Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁))
                ∘ cw-∂-before-Susp))
            (Bouquet-to-Xₙ/Xₙ₋₁-in-merid-β skel <I x) ⟩
    ap ( Susp-fmap (fwproj <I₋₁)
       ∘ Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁))
       ∘ cw-∂-before-Susp)
       (cfglue (attaching-last skel <I x) ∙' ap cfcod (spoke <I x))
      =⟨ ap-∘
          ( Susp-fmap (fwproj <I₋₁)
          ∘ Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁)))
          cw-∂-before-Susp
          (cfglue (attaching-last skel <I x) ∙' ap cfcod (spoke <I x)) ⟩
    ap ( Susp-fmap (fwproj <I₋₁)
       ∘ Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁)))
       (ap cw-∂-before-Susp
         (cfglue (attaching-last skel <I x) ∙' ap cfcod (spoke <I x)))
      =⟨ ap (ap ( Susp-fmap (fwproj <I₋₁)
                ∘ Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁))))
            ( ap-∙' cw-∂-before-Susp (cfglue (attaching-last skel <I x)) (ap cfcod (spoke <I x))
            ∙ ap2 _∙'_
                (cw-∂-before-Susp-glue-β (attaching-last skel <I x))
                ( ∘-ap cw-∂-before-Susp cfcod (spoke <I x)
                ∙ ap-cst south (spoke <I x))) ⟩
    ap ( Susp-fmap (fwproj <I₋₁)
       ∘ Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁)))
       (merid (cfcod (attaching-last skel <I x)))
      =⟨ ap-∘
          (Susp-fmap (fwproj <I₋₁))
          (Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁)))
          (merid (cfcod (attaching-last skel <I x))) ⟩
    ap (Susp-fmap (fwproj <I₋₁))
       (ap (Susp-fmap (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁)))
           (merid (cfcod (attaching-last skel <I x))))
      =⟨ ap
          (ap (Susp-fmap (fwproj <I₋₁)))
          (SuspFmap.merid-β
            (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁))
            (cfcod (attaching-last skel <I x))) ⟩
    ap (Susp-fmap (fwproj <I₋₁))
       (merid (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁) (cfcod (attaching-last skel <I x))))
      =⟨ SuspFmap.merid-β (fwproj <I₋₁)
          (<– (Bouquet-equiv-Xₙ/Xₙ₋₁ skel₋₁) (cfcod (attaching-last skel <I x))) ⟩
    merid (function₁ <I <I₋₁ x)
      =⟨ ! $ SuspFmap.merid-β (function₁ <I <I₋₁) x ⟩
    ap (Susp-fmap (function₁ <I <I₋₁)) (merid x)
      =∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Bin-embedding where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties using (+-identityʳ; +-suc; +-comm; +-assoc)

open import Isomorphism using (_≲_)

-- 2進数の表現
data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

-- 2進数のインクリメント
inc : Bin → Bin
inc ⟨⟩    = ⟨⟩ I
inc (b O) = b I
inc (b I) = inc b O

-- 自然数から2進数への変換
to : ℕ → Bin
to zero    = ⟨⟩ O
to (suc n) = inc (to n)

-- 2進数から自然数への変換
from : Bin → ℕ
from ⟨⟩    = zero
from (b O) = 2 * (from b)
from (b I) = 2 * (from b) + 1

2*n≡n+n : ∀ (n : ℕ) → 2 * n ≡ n + n
2*n≡n+n n rewrite +-identityʳ n = refl

+-suc-suc : ∀ (m n : ℕ) → (suc m) + (suc n) ≡ suc (suc (m + n))
+-suc-suc m n rewrite +-suc (suc m) n | +-assoc 1 m n = refl

from∘inc≡suc∘from : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
from∘inc≡suc∘from ⟨⟩ = refl
from∘inc≡suc∘from (b O) rewrite +-suc (from (b O)) zero = cong suc (+-identityʳ (from (b O)))
from∘inc≡suc∘from (b I) rewrite from∘inc≡suc∘from b | 2*n≡n+n (suc (from b)) | +-suc-suc (from b) (from b) | sym (2*n≡n+n (from b)) | +-comm 1 (2 * (from b)) = refl

from∘to : ∀ (n : ℕ) → from (to n) ≡ n
from∘to zero = refl
from∘to (suc n) rewrite from∘inc≡suc∘from (to n) = cong suc (from∘to n)

Bin-embedding : ℕ ≲ Bin
Bin-embedding =
  record
    { to      = to
    ; from    = from
    ; from∘to = from∘to
    }

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

postulate
  _↦_ : ∀ {i} {A : Set i} → A → A → Set i
  idr : ∀ {i} {A : Set i} {a : A} → a ↦ a
{-# BUILTIN REWRITE _↦_ #-}

data _==_ {i} {A : Set i} (a : A) : A → Set i where
  idp : a == a

PathOver : ∀ {i j} {A : Set i} (B : A → Set j)
  {x y : A} (p : x == y) (u : B x) (v : B y) → Set j
PathOver B idp u v = (u == v)

syntax PathOver B p u v =
  u == v [ B ↓ p ]

postulate
  PathOver-rewr : ∀ {i j} {A : Set i} {B : Set j} {x y : A} (p : x == y) (u v : B) →
    (PathOver (λ _ → B) p u v) ↦ (u == v)
  {-# REWRITE PathOver-rewr #-}

ap : ∀ {i j} {A : Set i} {B : A → Set j} (f : (a : A) → B a) {x y : A}
  → (p : x == y) → PathOver B p (f x) (f y)
ap f idp = idp

postulate
  Circle : Set
  base : Circle
  loop : base == base

module _ {i} {P : Circle → Set i} (base* : P base) (loop* : base* == base* [ P ↓ loop ])
 where
  postulate
    Circle-elim : (x : Circle) → P x
    Circle-base-β : Circle-elim base ↦ base*
    {-# REWRITE Circle-base-β #-}
    Circle-loop-β : ap Circle-elim loop ↦ loop*
    {-# REWRITE Circle-loop-β #-}

idCircle : Circle → Circle
idCircle = Circle-elim base loop


text:
kk : ∀ {ℓ} → Set ℓ
kk = {!∀ B → B!}


text:
module plfa.part1.Connectives where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality)
open plfa.part1.Isomorphism.≃-Reasoning

data _×_ (A B : Set) : Set where

  ⟨_,_⟩ :
      A
    → B
      -----
    → A × B

proj₁ : ∀ {A B : Set}
  → A × B
    -----
  → A
proj₁ ⟨ x , y ⟩ = x

proj₂ : ∀ {A B : Set}
  → A × B
    -----
  → B
proj₂ ⟨ x , y ⟩ = y

η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ x , y ⟩ = refl

infixr 2 _×_

record _×′_ (A B : Set) : Set where
  constructor ⟨_,_⟩′
  field
    proj₁′ : A
    proj₂′ : B
open _×′_

η-×′ : ∀ {A B : Set} (w : A ×′ B) → ⟨ proj₁′ w , proj₂′ w ⟩′ ≡ w
η-×′ w = refl

data Bool : Set where
  true  : Bool
  false : Bool

data Tri : Set where
  aa : Tri
  bb : Tri
  cc : Tri

×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm =
  record
    { to       =  λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
    ; from     =  λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
    ; from∘to  =  λ{ ⟨ x , y ⟩ → refl }
    ; to∘from  =  λ{ ⟨ y , x ⟩ → refl }
    }

×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
×-assoc =
  record
    { to      = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ }
    ; from    = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
    ; from∘to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → refl }
    ; to∘from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → refl }
    }

data ⊤ : Set where

  tt :
    --
    ⊤

η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ tt = refl

record ⊤′ : Set where
  constructor tt′

η-⊤′ : ∀ (w : ⊤′) → tt′ ≡ w
η-⊤′ w = refl

truth′ : ⊤′
truth′ = _

⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
⊤-identityˡ =
  record
    { to      = λ{ ⟨ tt , x ⟩ → x }
    ; from    = λ{ x → ⟨ tt , x ⟩ }
    ; from∘to = λ{ ⟨ tt , x ⟩ → refl }
    ; to∘from = λ{ x → refl }
    }

⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
⊤-identityʳ {A} =
  ≃-begin
    (A × ⊤)
  ≃⟨ ×-comm ⟩
    (⊤ × A)
  ≃⟨ ⊤-identityˡ ⟩
    A
  ≃-∎

data _⊎_ (A B : Set) : Set where

  inj₁ :
      A
      -----
    → A ⊎ B

  inj₂ :
      B
      -----
    → A ⊎ B

case-⊎ : ∀ {A B C : Set}
  → (A → C)
  → (B → C)
  → A ⊎ B
    -----------
  → C
case-⊎ f g (inj₁ x) = f x
case-⊎ f g (inj₂ y) = g y

η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
η-⊎ (inj₁ x) = refl
η-⊎ (inj₂ y) = refl

uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) →
  case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
uniq-⊎ h (inj₁ x) = refl
uniq-⊎ h (inj₂ y) = refl

infixr 1 _⊎_

⊎-comm : ∀ {A B : Set} → A ⊎ B ≃ B ⊎ A
⊎-comm = record {
  to = λ { (inj₁ x) → inj₂ x ; (inj₂ x) → inj₁ x };
  from = λ { (inj₁ x) → inj₂ x ; (inj₂ x) → inj₁ x};
  from∘to = λ { (inj₁ x) → refl ; (inj₂ x) → refl} ;
  to∘from = λ { (inj₁ x) → refl ; (inj₂ x) → refl} }

⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
⊎-assoc = record {
                 to = λ { (inj₁ (inj₁ x)) → inj₁ x ;
                          (inj₁ (inj₂ x)) → inj₂ (inj₁ x) ;
                          (inj₂ x) → inj₂ (inj₂ x)} ;
                 from = λ { (inj₁ x) → inj₁ (inj₁ x) ;
                            (inj₂ (inj₁ x)) → inj₁ (inj₂ x) ;
                            (inj₂ (inj₂ x)) → inj₂ x} ;
                 from∘to = λ { (inj₁ (inj₁ x)) → refl ;
                               (inj₁ (inj₂ x)) → refl ;
                                (inj₂ x) → refl} ;
                 to∘from = λ { (inj₁ x) → refl ;
                               (inj₂ (inj₁ x)) → refl;
                               (inj₂ (inj₂ x)) → refl}
                 }

data ⊥ : Set where

⊥-elim : ∀ {A : Set}
  → ⊥
    --
  → A
⊥-elim ()

uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
uniq-⊥ h ()

⊥-count : ⊥ → ℕ
⊥-count ()

→-elim : ∀ {A B : Set}
  → (A → B)
  → A
    -------
  → B
→-elim L M = L M

η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
η-→ f = refl

currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
currying =
  record
    { to      =  λ{ f → λ{ ⟨ x , y ⟩ → f x y }}
    ; from    =  λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}}
    ; from∘to =  λ{ f → refl }
    ; to∘from =  λ{ g → extensionality λ{ ⟨ x , y ⟩ → refl }}
    }

→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-distrib-⊎ =
  record
    { to      = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }
    ; from    = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
    ; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }
    ; to∘from = λ{ ⟨ g , h ⟩ → refl }
    }

→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× =
  record
    { to      = λ{ f → ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩ }
    ; from    = λ{ ⟨ g , h ⟩ → λ x → ⟨ g x , h x ⟩ }
    ; from∘to = λ{ f → extensionality λ{ x → η-× (f x) } }
    ; to∘from = λ{ ⟨ g , h ⟩ → refl }
    }

×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
×-distrib-⊎ =
  record
    { to      = λ{ ⟨ inj₁ x , z ⟩ → (inj₁ ⟨ x , z ⟩)
                 ; ⟨ inj₂ y , z ⟩ → (inj₂ ⟨ y , z ⟩)
                 }
    ; from    = λ{ (inj₁ ⟨ x , z ⟩) → ⟨ inj₁ x , z ⟩
                 ; (inj₂ ⟨ y , z ⟩) → ⟨ inj₂ y , z ⟩
                 }
    ; from∘to = λ{ ⟨ inj₁ x , z ⟩ → refl
                 ; ⟨ inj₂ y , z ⟩ → refl
                 }
    ; to∘from = λ{ (inj₁ ⟨ x , z ⟩) → refl
                 ; (inj₂ ⟨ y , z ⟩) → refl
                 }
    }

⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
⊎-distrib-× =
  record
    { to      = λ{ (inj₁ ⟨ x , y ⟩) → ⟨ inj₁ x , inj₁ y ⟩
                 ; (inj₂ z)         → ⟨ inj₂ z , inj₂ z ⟩
                 }
    ; from    = λ{ ⟨ inj₁ x , inj₁ y ⟩ → (inj₁ ⟨ x , y ⟩)
                 ; ⟨ inj₁ x , inj₂ z ⟩ → (inj₂ z)
                 ; ⟨ inj₂ z , _      ⟩ → (inj₂ z)
                 }
    ; from∘to = λ{ (inj₁ ⟨ x , y ⟩) → refl
                 ; (inj₂ z)         → refl
                 }
    }

⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
⊎-weak-× ⟨ inj₁ x , y ⟩ = inj₁ x
⊎-weak-× ⟨ inj₂ x , y ⟩ = inj₂ ⟨ x , y ⟩

⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
⊎×-implies-×⊎ (inj₁ ⟨ x , y ⟩) = ⟨ inj₁ x , inj₁ y ⟩
⊎×-implies-×⊎ (inj₂ ⟨ x , y ⟩) = ⟨ (inj₂ x) , (inj₂ y) ⟩

max_stars_repo_name: UnsoundWitch/proofs

max_issues_repo_name: sym-cereal/proofs

max_forks_repo_name: sym-cereal/proofs


text:
module _ where

open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

variable
  a b : Set

{-# FOREIGN AGDA2HS
  import Prelude hiding (map, sum)
 #-}

data Exp (v : Set) : Set where
  Plus : Exp v → Exp v → Exp v
  Int : Nat → Exp v
  Var : v → Exp v

{-# COMPILE AGDA2HS Exp #-}

eval : (a → Nat) → Exp a → Nat
eval env (Plus a b) = eval env a + eval env b
eval env (Int n) = n
eval env (Var x) = env x

{-# COMPILE AGDA2HS eval #-}

sum : List Nat → Nat
sum []       = 0
sum (x ∷ xs) = x + sum xs

{-# COMPILE AGDA2HS sum #-}

{-# FOREIGN AGDA2HS -- comment #-}

append : List a → List a → List a
append []       ys = ys
append (x ∷ xs) ys = x ∷ append xs ys

{-# COMPILE AGDA2HS append #-}

map : (a → b) → List a → List b
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

{-# COMPILE AGDA2HS map #-}

assoc : (a b c : Nat) → a + (b + c) ≡ (a + b) + c
assoc zero    b c = refl
assoc (suc a) b c rewrite assoc a b c = refl

thm : ∀ xs ys → sum (append xs ys) ≡ sum xs + sum ys
thm []       ys = refl
thm (x ∷ xs) ys rewrite thm xs ys | assoc x (sum xs) (sum ys) = refl


text:
module Functors.Fin where

open import Library
open import Categories.Sets
open import Categories.Setoids
open import Categories
open import Categories.Initial
open import Categories.CoProducts
open import Functors
open import Isomorphism
open import Functors.FullyFaithful

open Cat
open Fun
open Iso

Nats : Cat {lzero}{lzero}
Nats = record{
  Obj  = ℕ;
  Hom  = λ m n → Fin m → Fin n;
  iden = id;
  comp = λ f g → f ∘ g;
  idl  = refl;
  idr  = refl;
  ass  = refl}

-- initial object

initN : Init Nats zero
initN = record {
  i   = λ ();
  law = ext λ ()}

-- coproducts

extend : ∀ {m n} -> Fin m -> Fin (m + n)
extend zero    = zero
extend (suc i) = suc (extend i)

lift : ∀ m {n} -> Fin n -> Fin (m + n)
lift zero    i = i
lift (suc m) i = suc (lift m i)

case : ∀ (m : ℕ){n : ℕ}{X : Set} →
  (Fin m → X) → (Fin n → X) → Fin (m + n) → X
case zero    f g i       = g i
case (suc m) f g zero    = f zero
case (suc m) f g (suc i) = case m (f ∘ suc) g i

lem1 : ∀ A {B C}(f : Fin A → C) (g : Fin B → C)(i : Fin A) →
  case A f g (extend i) ≅ f i
lem1 zero f g ()
lem1 (suc A) f g zero    = refl
lem1 (suc A) f g (suc i) = lem1 A (f ∘ suc) g i

lem2 : ∀ A {B C} (f : Fin A → C) (g : Fin B → C)(i : Fin B) →
  case A f g (lift A i) ≅ g i
lem2 zero f g zero    = refl
lem2 zero f g (suc i) = refl
lem2 (suc A) f g i    = lem2 A (f ∘ suc) g i

lem3 : ∀ A {B C}(f : Fin A → C) (g : Fin B → C)
  (h : Fin (A + B) → C) →
  (λ x → h (extend {A} x)) ≅ f →
  (λ x → h (lift A x)) ≅ g → ∀ i → h i ≅ case A f g i
lem3 zero    f g h p q i       = fcong i q
lem3 (suc A) f g h p q zero    = fcong zero p
lem3 (suc A) f g h p q (suc i) =
  lem3 A (f ∘ suc) g (h ∘ suc) (ext (λ i → fcong (suc i) p)) q i

coprod : CoProd Nats
coprod = record
  { _+_   = _+_
  ; inl   = extend
  ; inr   = λ{m} → lift m
  ; [_,_] = λ{m} → case m
  ; law1  = λ{m} f g → ext (lem1 m f g)
  ; law2  = λ{m} f g → ext (lem2 m f g)
  ; law3  = λ{m} f g h p q → ext (lem3 m f g h p q)
  }

--

FinF : Fun Nats Sets
FinF = record {
  OMap  = Fin;
  HMap  = id;
  fid   = refl;
  fcomp = refl}

FinFoid : Fun Nats Setoids
FinFoid = record {
  OMap  = λ n → record {
    set  = Fin n ;
    eq   = λ i j → i ≅ j;
    ref  = refl;
    sym' = sym;
    trn  = trans};
  HMap  = λ f → record {
    fun = f; feq = cong f};
  fid   = SetoidFunEq refl (iext λ _ → iext λ _ → ext congid);
  fcomp = λ{_ _ _ f g} →
    SetoidFunEq refl (iext λ _ → iext λ _ → ext (congcomp f g))}

FinFF : FullyFaithful FinF
FinFF X Y = record {
  fun  = id;
  inv  = id;
  law1 = λ _ → refl;
  law2 = λ _ → refl}

open import Data.Bool

feq : forall {n} -> Fin n -> Fin n -> Bool
feq zero    zero    = true
feq zero    (suc j) = false
feq (suc i) zero    = false
feq (suc i) (suc j) = true

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.SumFin where

open import Cubical.Data.SumFin.Base public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
-- Andreas, 2016-10-14, issue #2260 testcase by Nisse

-- {-# OPTIONS -v tc.meta:40 #-}

data D : Set → Set₁ where
  d : (A : Set) → D A

postulate
  A : Set
  f : (A : Set) → D A → D A

B : Set₁
B = Set
  where
  abstract

    A′ : Set
    A′ = A

  x : D A′
  x = f _ (d A′)

-- WAS: internal error
-- should check


text:
------------------------------------------------------------------------
-- A comparison of the two definitions of bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Bisimilarity.Comparison where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (Unit)

open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Fin equality-with-J
open import Function-universe equality-with-J hiding (_∘_; id)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import Nat equality-with-J as Nat
open import Surjection equality-with-J using (_↠_)

import Bisimilarity
import Bisimilarity.Classical
import Bisimilarity.Classical.Equational-reasoning-instances
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning
import Indexed-container as IC
open import Labelled-transition-system
open import Relation

module _ {ℓ} {lts : LTS ℓ} where

  open LTS lts

  private
    module Cl = Bisimilarity.Classical lts
    module Co = Bisimilarity           lts

  -- Classically bisimilar processes are coinductively bisimilar.

  cl⇒co : ∀ {i p q} → p Cl.∼ q → Co.[ i ] p ∼ q
  cl⇒co = IC.gfp⊆ν ℓ

  -- Coinductively bisimilar processes are classically bisimilar.

  co⇒cl : ∀ {p q} → p Co.∼ q → p Cl.∼ q
  co⇒cl = IC.ν⊆gfp ℓ

  -- The function cl⇒co is a left inverse of co⇒cl (up to pointwise
  -- bisimilarity).

  cl⇒co∘co⇒cl : ∀ {i p q}
                (p∼q : p Co.∼ q) →
                Co.[ i ] cl⇒co (co⇒cl p∼q) ≡ p∼q
  cl⇒co∘co⇒cl p∼q = IC.gfp⊆ν∘ν⊆gfp ℓ p∼q

  -- If there are two processes that are not equal, but bisimilar,
  -- then co⇒cl is not a left inverse of cl⇒co.

  co⇒cl∘cl⇒co : ∀ {p q} →
                p ≢ q → p Co.∼ q →
                ∃ λ (p∼p : p Cl.∼ p) → co⇒cl (cl⇒co p∼p) ≢ p∼p
  co⇒cl∘cl⇒co {p} {q} p≢q p∼q =
      reflexive

    , (co⇒cl (cl⇒co reflexive) ≡ reflexive  ↝⟨ cong (λ R → proj₁ R (p , q)) ⟩
       ↑ _ (p Co.∼ q) ≡ ↑ _ (p ≡ q)         ↝⟨ (λ eq → ≡⇒↝ _ eq $ lift p∼q) ⟩
       ↑ _ (p ≡ q)                          ↔⟨ Bijection.↑↔ ⟩
       p ≡ q                                ↝⟨ p≢q ⟩□
       ⊥                                    □)

  -- The two definitions of bisimilarity are logically equivalent.

  classical⇔coinductive : ∀ {p q} → p Cl.∼ q ⇔ p Co.∼ q
  classical⇔coinductive = IC.gfp⇔ν ℓ

  -- There is a split surjection from the classical definition of
  -- bisimilarity to the coinductive one (assuming two kinds of
  -- extensionality).

  classical↠coinductive :
    Extensionality ℓ ℓ →
    Co.Extensionality →
    ∀ {p q} → p Cl.∼ q ↠ p Co.∼ q
  classical↠coinductive ext co-ext = IC.gfp↠ν ext ℓ co-ext

-- There is at least one LTS for which there is a split surjection
-- from the coinductive definition of bisimilarity to the classical
-- one.

coinductive↠classical :
  ∀ {p q} →
  Bisimilarity._∼_           empty p q ↠
  Bisimilarity.Classical._∼_ empty p q
coinductive↠classical {p = ()}

-- There is an LTS for which coinductive bisimilarity is pointwise
-- propositional (assuming two kinds of extensionality).

coinductive-bisimilarity-is-sometimes-propositional :
  Extensionality lzero lzero →
  let module Co = Bisimilarity one-loop in
  Co.Extensionality → Is-proposition (tt Co.∼ tt)
coinductive-bisimilarity-is-sometimes-propositional ext co-ext ∼₁ ∼₂ =
  extensionality ext co-ext (irr ∼₁ ∼₂)
  where
  open Bisimilarity one-loop

  irr : ∀ {i} ∼₁ ∼₂ → [ i ] ∼₁ ≡ ∼₂
  irr ∼₁ ∼₂ =
    Bisimilarity-of-∼.⟨ ext
                      , ∼₁
                      , ∼₂
                      , (λ _ → refl , refl , irr′ (proj₂ ∼₁ _)
                                                  (proj₂ ∼₂ _))
                      , (λ _ → refl , refl , irr′ (proj₂ ∼₁ _)
                                                  (proj₂ ∼₂ _))
                      ⟩
    where
    irr′ : ∀ {i} ∼₁ ∼₂ → [ i ] ∼₁ ≡′ ∼₂
    force (irr′ ∼₁ ∼₂) = irr (force ∼₁) (force ∼₂)

-- However, classical bisimilarity (of any size) is, for the same LTS,
-- not pointwise propositional.

classical-bisimilarity-is-not-propositional :
  let module Cl = Bisimilarity.Classical one-loop in
  ∀ {ℓ} → ¬ Is-proposition (Cl.Bisimilarity′ ℓ (tt , tt))
classical-bisimilarity-is-not-propositional {ℓ} =
  Is-proposition (Bisimilarity′ ℓ (tt , tt))    ↝⟨ (λ f → f tt∼tt₁ tt∼tt₂) ⟩
  tt∼tt₁ ≡ tt∼tt₂                               ↝⟨ cong (λ R → proj₁ R (tt , tt)) ⟩
  Unit ≡ (Unit ⊎ Unit)                          ↝⟨ (λ eq → Fin 1          ↝⟨ inverse Unit↔Fin1 ⟩
                                                           Unit           ↝⟨ ≡⇒↝ _ eq ⟩
                                                           Unit ⊎ Unit    ↝⟨ Unit↔Fin1 ⊎-cong Unit↔Fin1 ⟩
                                                           Fin 1 ⊎ Fin 1  ↝⟨ Fin⊎Fin↔Fin+ 1 1 ⟩□
                                                           Fin 2          □) ⟩
  Fin 1 ↔ Fin 2                                 ↝⟨ _⇔_.to isomorphic-same-size ⟩
  1 ≡ 2                                         ↝⟨ from-⊎ (1 Nat.≟ 2) ⟩□
  ⊥                                             □
  where
  open Bisimilarity.Classical one-loop

  tt∼tt₁ : Bisimilarity′ ℓ (tt , tt)
  tt∼tt₁ = reflexive-∼′ _

  tt∼tt₂ : Bisimilarity′ ℓ (tt , tt)
  tt∼tt₂ =
    let R , R-is-a-bisimulation , ttRtt =
          _⇔_.to (Bisimilarity′↔ _ _) tt∼tt₁ in
    _⇔_.from (Bisimilarity′↔ _ _)
      ( (R ∪ R)
      , ×2-preserves-bisimulations R-is-a-bisimulation
      , inj₁ ttRtt
      )

  Unit = ↑ ℓ (tt ≡ tt)

  Unit↔Fin1 =
    Unit     ↔⟨ Bijection.↑↔ ⟩
    tt ≡ tt  ↝⟨ _⇔_.to contractible⇔↔⊤ (+⇒≡ $ mono₁ 0 ⊤-contractible) ⟩
    ⊤        ↝⟨ inverse ⊎-right-identity ⟩□
    Fin 1    □

-- Thus, assuming two kinds of extensionality, there is in general no
-- split surjection from the coinductive definition of bisimilarity to
-- the classical one (of any size).

¬coinductive↠classical :
  Extensionality lzero lzero →
  Bisimilarity.Extensionality one-loop →
  ∀ {ℓ} →
  ¬ (∀ {p q} → Bisimilarity._∼_                     one-loop    p   q ↠
               Bisimilarity.Classical.Bisimilarity′ one-loop ℓ (p , q))
¬coinductive↠classical ext co-ext {ℓ} =
  (∀ {p q} → p Co.∼ q ↠ Cl.Bisimilarity′ ℓ (p , q))  ↝⟨ (λ co↠cl → co↠cl {q = _}) ⟩

  tt Co.∼ tt ↠ Cl.Bisimilarity′ ℓ (tt , tt)          ↝⟨ (λ co↠cl → H-level.respects-surjection co↠cl 1) ⟩

  (Is-proposition (tt Co.∼ tt) →
   Is-proposition (Cl.Bisimilarity′ ℓ (tt , tt)))    ↝⟨ (_$ coinductive-bisimilarity-is-sometimes-propositional ext co-ext) ⟩

  Is-proposition (Cl.Bisimilarity′ ℓ (tt , tt))      ↝⟨ classical-bisimilarity-is-not-propositional ⟩□

  ⊥                                                  □
  where
  module Cl = Bisimilarity.Classical one-loop
  module Co = Bisimilarity           one-loop

-- Note also that coinductive bisimilarity is not always
-- propositional.

coinductive-bisimilarity-is-not-propositional :
  let open Bisimilarity two-bisimilar-processes in
  ¬ (∀ {p q} → Is-proposition (p ∼ q))
coinductive-bisimilarity-is-not-propositional =
  (∀ {p q} → Is-proposition (p ∼ q))            ↝⟨ (λ is-prop → is-prop {p = true} {q = true}) ⟩
  Is-proposition (true ∼ true)                  ↝⟨ (λ irr → irr _ _) ⟩
  proof true true true ≡ proof false true true  ↝⟨ cong (λ p → proj₁ (left-to-right {p = true} {q = true} p {p′ = true} _)) ⟩
  true ≡ false                                  ↝⟨ Bool.true≢false ⟩□
  ⊥                                             □
  where
  open Bisimilarity two-bisimilar-processes

  open import Indexed-container

  mutual
    proof : Bool → ∀ b₁ b₂ {i} → [ i ] b₁ ∼ b₂
    proof b b₁ b₂ =
      ⟨_,_⟩ {p = b₁} {q = b₂}
        (λ _ → b , _ , proof′ b _ _)
        (λ _ → b , _ , proof′ b _ _)

    proof′ : Bool → ∀ b₁ b₂ {i} → [ i ] b₁ ∼′ b₂
    force (proof′ b b₁ b₂) = proof b b₁ b₂

-- In fact, for every type A there is a pointwise split surjection
-- from a certain instance of bisimilarity (of any size) to equality
-- on A.

bisimilarity↠equality :
  ∀ {a} {A : Type a} →
  let open Bisimilarity (bisimilarity⇔equality A) in
  ∀ {i} {p q : A} → ([ i ] p ∼ q) ↠ p ≡ q
bisimilarity↠equality {A = A} {i} = record
  { logical-equivalence = record
    { to   = to
    ; from = from
    }
  ; right-inverse-of = to∘from
  }
  where
  open Bisimilarity (bisimilarity⇔equality A)

  to : ∀ {p q} → [ i ] p ∼ q → p ≡ q
  to p∼q with left-to-right p∼q (refl , refl)
  ... | _ , (refl , _) , _ = refl

  from : ∀ {p q} → p ≡ q → [ i ] p ∼ q
  from refl = reflexive

  to∘from : ∀ {p q} (p≡q : p ≡ q) → to (from p≡q) ≡ p≡q
  to∘from refl = refl

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category

-- Skew closed structure on a category
module SOAS.Construction.Skew.SkewClosed {o ℓ e} (C : Category o ℓ e) where

private
  module C = Category C
  open C
  variable
    A B X X′ Y Y′ Z Z′ U ℐ : Obj
    f g : A ⇒ B

  open Commutation C

open import Level
open import Data.Product using (Σ; _,_)
open import Function.Equality using (_⟶_)
open import Function.Inverse using (_InverseOf_; Inverse)

open import Categories.Category.Product
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.NaturalTransformation.Dinatural

record SkewClosed : Set (levelOfTerm C) where
  field
    -- internal hom
    [-,-] : Bifunctor C.op C C
    unit  : Obj

  [_,-] : Obj → Functor C C
  [_,-] = appˡ [-,-]

  [-,_] : Obj → Functor C.op C
  [-,_] = appʳ [-,-]

  module [-,-] = Functor [-,-]

  [_,_]₀ : Obj → Obj → Obj
  [ X , Y ]₀ = [-,-].F₀ (X , Y)

  [_,_]₁ : A ⇒ B → X ⇒ Y → [ B , X ]₀ ⇒ [ A , Y ]₀
  [ f , g ]₁ = [-,-].F₁ (f , g)

  field
    -- i
    identity : NaturalTransformation [ unit ,-] idF
    -- j
    diagonal : Extranaturalʳ unit [-,-]

  module identity = NaturalTransformation identity
  module diagonal = DinaturalTransformation diagonal

  [[X,-],[X,-]] : Obj → Bifunctor C.op C C
  [[X,-],[X,-]] X = [-,-] ∘F (Functor.op [ X ,-] ⁂ [ X ,-])

  [[-,Y],[-,Z]] : Obj → Obj → Bifunctor C C.op C
  [[-,Y],[-,Z]] Y Z = [-,-] ∘F ((Functor.op [-, Y ]) ⁂ [-, Z ])

  -- L needs to be natural in Y and Z.
  -- it is better to spell out the conditions and then prove that indeed
  -- the naturality conditions hold.
  field
    L : ∀ X Y Z → [ Y , Z ]₀ ⇒ [ [ X , Y ]₀ , [ X , Z ]₀ ]₀
    L-commute : [ [ Y , Z ]₀ ⇒  [ [ X , Y′ ]₀ , [ X , Z′ ]₀ ]₀ ]⟨
                  [ f , g ]₁                          ⇒⟨ [ Y′ , Z′ ]₀ ⟩
                  L X Y′ Z′
                ≈ L X Y Z                             ⇒⟨ [ [ X , Y ]₀ , [ X , Z ]₀ ]₀ ⟩
                  [ [ C.id , f ]₁ , [ C.id , g ]₁ ]₁
                ⟩

  L-natural : NaturalTransformation [-,-] ([[X,-],[X,-]] X)
  L-natural {X} = ntHelper record
    { η       = λ where
      (Y , Z) → L X Y Z
    ; commute = λ _ → L-commute
    }

  module L-natural {X}     = NaturalTransformation (L-natural {X})

  -- other required diagrams
  field
    Lj≈j : [ unit ⇒ [ [ X , Y ]₀ , [ X , Y ]₀ ]₀ ]⟨
             diagonal.α  Y                  ⇒⟨ [ Y , Y ]₀ ⟩
             L X Y Y
           ≈ diagonal.α [ X , Y ]₀
           ⟩
    ijL≈id : [ [ X , Y ]₀ ⇒ [ X , Y ]₀ ]⟨
             L X X Y                   ⇒⟨ [ [ X , X ]₀ , [ X , Y ]₀ ]₀ ⟩
             [ diagonal.α X , C.id ]₁  ⇒⟨ [ unit , [ X , Y ]₀ ]₀ ⟩
             identity.η [ X , Y ]₀
           ≈ C.id
           ⟩
    iL≈i : [ [ Y , Z ]₀ ⇒ [ [ unit , Y ]₀ , Z ]₀ ]⟨
             L unit Y Z                ⇒⟨ [ [ unit , Y ]₀ , [ unit , Z ]₀ ]₀ ⟩
             [ C.id , identity.η Z ]₁
           ≈ [ identity.η Y , C.id ]₁
           ⟩

    ij≈id : [ unit ⇒ unit ]⟨
             diagonal.α unit    ⇒⟨ [ unit , unit ]₀ ⟩
             identity.η unit
           ≈ C.id
           ⟩

    pentagon : [ [ U , ℐ ]₀ ⇒ [ [ Y , U ]₀ , [ [ X , Y ]₀ , [ X , ℐ ]₀ ]₀ ]₀ ]⟨
                 L X U ℐ                            ⇒⟨ [ [ X , U ]₀ , [ X , ℐ ]₀ ]₀ ⟩
                 L [ X , Y ]₀ [ X , U ]₀ [ X , ℐ ]₀ ⇒⟨ [ [ [ X , Y ]₀ , [ X , U ]₀ ]₀ , [ [ X , Y ]₀ , [ X , ℐ ]₀ ]₀ ]₀ ⟩
                 [ L X Y U , C.id ]₁
               ≈ L Y U ℐ                            ⇒⟨ [ [ Y , U ]₀ , [ Y , ℐ ]₀ ]₀ ⟩
                 [ C.id , L X Y ℐ ]₁
               ⟩

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Categories.Setoids where

open import Library
open import Categories

record Setoid {a b} : Set (lsuc (a ⊔ b)) where
  field set : Set a
        eq  : set → set → Set b
        ref : {s : set} → eq s s
        sym' : {s s' : set} → eq s s' → eq s' s
        trn : {s s' s'' : set} →
              eq s s' → eq s' s'' → eq s s''
open Setoid

record SetoidFun (S S' : Setoid) : Set where
  constructor setoidfun
  field fun : set S → set S'
        feq : {s s' : set S} →
              eq S s s' → eq S' (fun s) (fun s')
open SetoidFun

SetoidFunEq : {S S' : Setoid}{f g : SetoidFun S S'} →
              fun f ≅ fun g →
              (λ{s}{s'}(p : eq S s s') → feq f p)
              ≅
              (λ{s}{s'}(p : eq S s s') → feq g p) →
              f ≅ g
SetoidFunEq {f = setoidfun fun feq} {setoidfun .fun .feq} refl refl = refl

idFun : {S : Setoid} → SetoidFun S S
idFun = record {fun = id; feq = id}

compFun : {S S' S'' : Setoid} →
          SetoidFun S' S'' → SetoidFun S S' → SetoidFun S S''
compFun f g = record {fun = fun f ∘ fun g; feq = feq f ∘ feq g}

idl : {X Y : Setoid} {f : SetoidFun X Y} → compFun idFun f ≅ f
idl {f = setoidfun _ _} = refl

idr : {X Y : Setoid} {f : SetoidFun X Y} → compFun f idFun ≅ f
idr {f =  setoidfun _ _} = refl

Setoids : Cat
Setoids = record{
  Obj  = Setoid;
  Hom  = SetoidFun;
  iden = idFun;
  comp = compFun;
  idl  = idl;
  idr  = idr;
  ass  = refl}
-- -}


text:
------------------------------------------------------------------------
-- Divisibility and coprimality
------------------------------------------------------------------------

module Data.Integer.Divisibility where

open import Data.Function
open import Data.Integer
open import Data.Integer.Properties
import Data.Nat.Divisibility as ℕ
import Data.Nat.Coprimality as ℕ
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

-- Divisibility.

infix 4 _∣_

_∣_ : Rel ℤ
_∣_ = ℕ._∣_ on₁ ∣_∣

-- Coprimality.

Coprime : Rel ℤ
Coprime = ℕ.Coprime on₁ ∣_∣

-- If i divides jk and is coprime to j, then it divides k.

coprime-divisor : ∀ i j k → Coprime i j → i ∣ j * k → i ∣ k
coprime-divisor i j k c eq =
  ℕ.coprime-divisor c (subst (ℕ._∣_ ∣ i ∣) (abs-*-commute j k) eq)


text:
module Issue18 where

postulate
  D : Set

data ∃ (A : D → Set) : Set where
  _,_ : (witness : D) → A witness → ∃ A

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --cubical #-}
module Cubical.README where

------------------------------------------------------------------------
-- An experimental library for Cubical Agda
-----------------------------------------------------------------------

-- The library comes with a .agda-lib file, for use with the library
-- management system.

------------------------------------------------------------------------
-- Module hierarchy
------------------------------------------------------------------------

-- The core library for Cubical Agda.
-- It contains basic primitives, equivalences, glue types.
import Cubical.Core.Everything

-- The foundations for Cubical Agda.
-- The Prelude module is self-explanatory.
import Cubical.Foundations.Prelude
import Cubical.Foundations.Everything

-- Data types and properties
import Cubical.Data.Everything

-- Properties and proofs about relations
import Cubical.Relation.Everything

-- Higher-inductive types
import Cubical.HITs.Everything

-- Coinductive data types and properties
import Cubical.Codata.Everything

-- Various experiments using Cubical Agda
import Cubical.Experiments.Everything


text:
module Lang.Function where

import      Lvl
open import Data.Boolean
open import Data.List as List using (List)
open import Data.List.Functions.Positional as List
open import Data.Option
open import Data
open import Lang.Reflection
open import Syntax.Do
open import Type

-- A default value tactic for implicit arguments.
-- This implements a "default arguments" language feature.
-- It works by always unifying the hole with the specified value.
-- Essentially a constant function for holes.
-- Example:
--   test : ∀{@(tactic default 𝑇) x : Bool} → Bool
--   test{x} = x
--   Now, `test = 𝑇`, `test{𝑇} = 𝑇`, `test{𝐹} = 𝐹`.
default : ∀{ℓ}{T : Type{ℓ}} → T → Term → TC(Unit{Lvl.𝟎})
default x hole = quoteTC x >>= unify hole

-- A no inferrance tactic for implicit arguments.
-- This makes implicit arguments work like explicit arguments by throwing an error when the hole does not match perfectly while still maintaining its implicit visibility status.
-- It works by always selecting the last argument in the hole, and the last argument is the one closest to the value, which is the argument one expects it to choose.
-- Examples:
--   idᵢwith : ∀{T : TYPE} → {@(tactic no-infer) x :  T} → T
--   idᵢwith {x = x} = x
--
--   idᵢwithout : ∀{T : TYPE} → {x :  T} → T
--   idᵢwithout {x = x} = x
--
--   postulate test : ({_ : Bool} → Bool) → Bool
--
--   test1 : Bool
--   test1 = test idᵢwith
--
--   test2 : (Bool → Bool) → Bool
--   test2 _ = test idᵢwith
--
--   test3 : ∀{T : TYPE} → {_ : T} → T
--   test3 = idᵢwith
--
--   It is useful in these kinds of scenarios because idᵢwithout would require writing the implicit argument explicitly, while idᵢwith always uses the given argument in order like how explicit arguments work.
no-infer : Term → TC(Unit{Lvl.𝟎})
no-infer hole@(meta _ args) with List.last(args)
... | None                                   = typeError (List.singleton (strErr "Expected a parameter with \"hidden\" visibility when using \"no-infer\", found none."))
... | Some (arg (arg-info hidden    _) term) = unify hole term
{-# CATCHALL #-}
... | Some (arg (arg-info _         _) term) = typeError (List.singleton (strErr "Wrong visibility of argument. Expected \"hidden\" when using \"no-infer\"."))
{-# CATCHALL #-}
no-infer _ = typeError (List.singleton (strErr "TODO: In what situations is this error occurring?"))

-- TODO: Implement idᵢwith, rename it to idᵢ, and put it in Functional. Also, try to refactor Data.Boolean, Data.List and Data.Option so that they only contain the type definition and its constructors. This minimizes the amount of dependencies this module requires (which should help in case of circular dependencies when importing this module).


text:
postulate
  T C D : Set
  instance I : {{_ : C}} → D
  d : {{_ : D}} → T

t : T
t = d


text:
{-# OPTIONS --without-K --safe #-}

module Categories.Diagram.Cone.Properties where

open import Level

open import Categories.Category
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.NaturalTransformation
import Categories.Diagram.Cone as Con
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D J J′ : Category o ℓ e

module _ {F : Functor J C} (G : Functor C D) where
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
    module CF = Con F
    GF = G ∘F F
    module CGF = Con GF

  F-map-Coneˡ : CF.Cone → CGF.Cone
  F-map-Coneˡ K = record
    { apex = record
      { ψ       = λ X → G.F₁ (ψ X)
      ; commute = λ f → [ G ]-resp-∘ (commute f)
      }
    }
    where open CF.Cone K

  F-map-Cone⇒ˡ : ∀ {K K′} (f : CF.Cone⇒ K K′) → CGF.Cone⇒ (F-map-Coneˡ K) (F-map-Coneˡ K′)
  F-map-Cone⇒ˡ f = record
    { arr     = G.F₁ arr
    ; commute = [ G ]-resp-∘ commute
    }
    where open CF.Cone⇒ f

module _ {F : Functor J C} (G : Functor J′ J) where
  private
    module C   = Category C
    module J′  = Category J′
    module F   = Functor F
    module G   = Functor G
    module CF  = Con F
    FG = F ∘F G
    module CFG = Con FG

  F-map-Coneʳ : CF.Cone → CFG.Cone
  F-map-Coneʳ K = record
    { apex = record
      { ψ       = λ j → ψ (G.F₀ j)
      ; commute = λ f → commute (G.F₁ f)
      }
    }
    where open CF.Cone K

  F-map-Cone⇒ʳ : ∀ {K K′} (f : CF.Cone⇒ K K′) → CFG.Cone⇒ (F-map-Coneʳ K) (F-map-Coneʳ K′)
  F-map-Cone⇒ʳ f = record
    { arr     = arr
    ; commute = commute
    }
    where open CF.Cone⇒ f

module _ {F G : Functor J C} (α : NaturalTransformation F G) where
  private
    module C  = Category C
    module J  = Category J
    module F  = Functor F
    module G  = Functor G
    module α  = NaturalTransformation α
    module CF = Con F
    module CG = Con G
    open C
    open HomReasoning
    open MR C

  nat-map-Cone : CF.Cone → CG.Cone
  nat-map-Cone K = record
    { apex = record
      { ψ       = λ j → α.η j C.∘ ψ j
      ; commute = λ {X Y} f → begin
        G.F₁ f ∘ α.η X ∘ ψ X ≈˘⟨ pushˡ (α.commute f) ⟩
        (α.η Y ∘ F.F₁ f) ∘ ψ X ≈⟨ pullʳ (commute f) ⟩
        α.η Y ∘ ψ Y ∎
      }
    }
    where open CF.Cone K

  nat-map-Cone⇒ : ∀ {K K′} (f : CF.Cone⇒ K K′) → CG.Cone⇒ (nat-map-Cone K) (nat-map-Cone K′)
  nat-map-Cone⇒ {K} {K′} f = record
    { arr     = arr
    ; commute = pullʳ commute
    }
    where open CF.Cone⇒ f

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --safe #-}

module Definition.Conversion.HelperDecidable where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Conversion
open import Definition.Conversion.Whnf
open import Definition.Conversion.Soundness
open import Definition.Conversion.Symmetry
open import Definition.Conversion.Stability
open import Definition.Conversion.Conversion
open import Definition.Conversion.Lift
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Reduction
open import Definition.Typed.Consequences.Equality
open import Definition.Typed.Consequences.Inequality as IE
open import Definition.Typed.Consequences.NeTypeEq
open import Definition.Typed.Consequences.SucCong

open import Tools.Nat
open import Tools.Product
open import Tools.Empty
open import Tools.Nullary
import Tools.PropositionalEquality as PE

dec-relevance : ∀ (r r′ : Relevance) → Dec (r PE.≡ r′)
dec-relevance ! ! = yes PE.refl
dec-relevance ! % = no (λ ())
dec-relevance % ! = no (λ ())
dec-relevance % % = yes PE.refl

dec-level : ∀ (l l′ : Level) → Dec (l PE.≡ l′)
dec-level ⁰ ⁰ = yes PE.refl
dec-level ⁰ ¹ = no (λ ())
dec-level ¹ ⁰ = no (λ ())
dec-level ¹ ¹ = yes PE.refl

-- Algorithmic equality of variables infers propositional equality.
strongVarEq : ∀ {m n A Γ l} → Γ ⊢ var n ~ var m ↑! A ^ l → n PE.≡ m
strongVarEq (var-refl x x≡y) = x≡y

-- Helper function for decidability of applications.
dec~↑!-app : ∀ {k k₁ l l₁ F F₁ G G₁ rF B Γ Δ lF lG lΠ lK}
          → ⊢ Γ ≡ Δ
          → Γ ⊢ k ∷ Π F ^ rF ° lF ▹ G ° lG ° lΠ ^ [ ! , ι lΠ ]
          → Δ ⊢ k₁ ∷ Π F₁ ^ rF ° lF ▹ G₁ ° lG ° lΠ ^ [ ! , ι lΠ ]
          → Γ ⊢ k ~ k₁ ↓! B ^ lK
          → Dec (Γ ⊢ l [genconv↑] l₁ ∷ F ^ [ rF , ι lF ])
          → Dec (∃ λ A → ∃ λ lA → Γ ⊢ k ∘ l ^ lΠ ~ k₁ ∘ l₁ ^ lΠ ↑! A ^ lA)
dec~↑!-app Γ≡Δ k k₁ k~k₁ (yes p) =
  let
    whnfA , neK , neL = ne~↓! k~k₁
    ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓! k~k₁)
    l≡l , ΠFG₁≡A = neTypeEq neK k ⊢k
    H , E , A≡ΠHE = Π≡A ΠFG₁≡A whnfA
    F≡H , rF≡rH , lF≡lH , lG≡lE , G₁≡E = injectivity (PE.subst (λ x → _ ⊢ _ ≡ x ^ _) A≡ΠHE ΠFG₁≡A)
  in yes (E [ _ ] , _ , app-cong (PE.subst₂ (λ x y → _ ⊢ _ ~ _ ↓! x ^ y) A≡ΠHE (PE.sym l≡l) k~k₁) (convConvTerm%! p F≡H))
dec~↑!-app Γ≡Δ k k₁ k~k₁ (no ¬p) = no (λ { (_ , _ ,  app-cong k~k₁′ p) →
  let
    whnfA , neK , neL = ne~↓! k~k₁′
    ⊢A , ⊢k , ⊢l = syntacticEqTerm (soundness~↓! k~k₁′)
    l≡l , Π≡Π = neTypeEq neK k ⊢k
    F≡F , rF≡rF , lF≡lF , lG≡lG , G≡G = injectivity Π≡Π
  in ¬p (convConvTerm%! (PE.subst₂ (λ x y → _ ⊢ _ [genconv↑] _ ∷ _ ^ [ x , ι y ]) (PE.sym rF≡rF) (PE.sym lF≡lF) p) (sym F≡F)) })

nonNeutralℕ : Neutral ℕ → ⊥
nonNeutralℕ ()

nonNeutralU : ∀ {r l} → Neutral (Univ r l) → ⊥
nonNeutralU ()

Idℕ-elim : ∀ {Γ l A B t u t' u'} → Neutral A → Γ ⊢ Id A t u ~ Id ℕ t' u' ↑! B ^ l → ⊥
Idℕ-elim neA (Id-cong x x₁ x₂) = let _ , _ , neℕ = ne~↓! x in ⊥-elim (nonNeutralℕ neℕ)
Idℕ-elim neA (Id-ℕ x x₁) = ⊥-elim (nonNeutralℕ neA)
Idℕ-elim neA (Id-ℕ0 x) = ⊥-elim (nonNeutralℕ neA)
Idℕ-elim neA (Id-ℕS x x₁) = ⊥-elim (nonNeutralℕ neA)

Idℕ-elim' : ∀ {Γ l A B t u t' u'} → Neutral A → Γ ⊢ Id ℕ t u ~ Id A t' u' ↑! B ^ l → ⊥
Idℕ-elim' neA e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in Idℕ-elim neA e'

conv↑-inversion : ∀ {Γ l A t u} → Whnf A → Whnf t → Whnf u → Γ ⊢ t [conv↑] u ∷ A ^ l → Γ ⊢ t [conv↓] u ∷ A ^ l
conv↑-inversion whnfA whnft whnfu ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
  let et = whnfRed*Term d whnft
      eu = whnfRed*Term d′ whnfu
      eA = whnfRed* D whnfA
  in PE.subst₃ (λ A X Y → _ ⊢ X [conv↓] Y ∷ A ^ _) (PE.sym eA) (PE.sym et) (PE.sym eu) t<>u

Idℕ0-elim- : ∀ {Γ l t} → Neutral t → Γ ⊢ t [conv↓] zero ∷ ℕ ^ l → ⊥
Idℕ0-elim- net (ℕ-ins ())
Idℕ0-elim- net (ne-ins x x₁ x₂ ())
Idℕ0-elim- () (zero-refl x)

Idℕ0-elim : ∀ {Γ l A t u u'} → Neutral t → Γ ⊢ Id ℕ t u ~ Id ℕ zero u' ↑! A ^ l → ⊥
Idℕ0-elim net (Id-cong x y x₂) =
  let e = conv↑-inversion ℕₙ (ne net) zeroₙ y in Idℕ0-elim- net e
Idℕ0-elim net (Id-ℕ () x₁)
Idℕ0-elim () (Id-ℕ0 x)

Idℕ0-elim' : ∀ {Γ l A t u u'} → Neutral t → Γ ⊢ Id ℕ zero u ~ Id ℕ t u' ↑! A ^ l → ⊥
Idℕ0-elim' net e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in Idℕ0-elim net e'

IdℕS-elim- : ∀ {Γ l t n} → Neutral t → Γ ⊢ t [conv↓] suc n ∷ ℕ ^ l → ⊥
IdℕS-elim- net (ℕ-ins ())
IdℕS-elim- net (ne-ins x x₁ x₂ ())
IdℕS-elim- () (suc-cong x)

IdℕS-elim : ∀ {Γ l A t u n u'} → Neutral t → Γ ⊢ Id ℕ t u ~ Id ℕ (suc n) u' ↑! A ^ l → ⊥
IdℕS-elim net (Id-cong x y x₂) =
  let e = conv↑-inversion ℕₙ (ne net) sucₙ y in IdℕS-elim- net e
IdℕS-elim net (Id-ℕ () x₁)
IdℕS-elim () (Id-ℕS x _)

IdℕS-elim' : ∀ {Γ l A t u n u'} → Neutral t → Γ ⊢ Id ℕ (suc n) u ~ Id ℕ t u' ↑! A ^ l → ⊥
IdℕS-elim' net e =  let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in IdℕS-elim net e'

Idℕ0S-elim- : ∀ {Γ l n} → Γ ⊢ zero [conv↓] suc n ∷ ℕ ^ l → ⊥
Idℕ0S-elim- (ℕ-ins ())
Idℕ0S-elim- (ne-ins x x₁ x₂ ())

Idℕ0S-elim : ∀ {Γ l A u u' n} → Γ ⊢ Id ℕ zero u ~ Id ℕ (suc n) u' ↑! A ^ l → ⊥
Idℕ0S-elim (Id-cong x y x₂) =
  let e = conv↑-inversion ℕₙ zeroₙ sucₙ y in Idℕ0S-elim- e
Idℕ0S-elim (Id-ℕ () _)

Idℕ0S-elim' : ∀ {Γ l A u u' n} → Γ ⊢ Id ℕ (suc n) u ~ Id ℕ zero u' ↑! A ^ l → ⊥
Idℕ0S-elim' e =  let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in Idℕ0S-elim e'

IdU-elim : ∀ {Γ l A B t u t' u' rU lU} → Neutral A → Γ ⊢ Id A t u ~ Id (Univ rU lU) t' u' ↑! B ^ l → ⊥
IdU-elim neA (Id-cong x x₁ x₂) = let _ , _ , neU = ne~↓! x in ⊥-elim (nonNeutralU neU)
IdU-elim neA (Id-U x x₁) = ⊥-elim (nonNeutralU neA)
IdU-elim neA (Id-Uℕ x) = ⊥-elim (nonNeutralU neA)
IdU-elim neA (Id-UΠ x x₁) = ⊥-elim (nonNeutralU neA)

IdU-elim' : ∀ {Γ l A B t u t' u' rU lU} → Neutral A → Γ ⊢ Id (Univ rU lU) t u ~ Id A t' u' ↑! B ^ l → ⊥
IdU-elim' neA e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in IdU-elim neA e'

IdUℕ-elim : ∀ {Γ l A t u t' u' rU lU} → Γ ⊢ Id (Univ rU lU) t u ~ Id ℕ t' u' ↑! A ^ l → ⊥
IdUℕ-elim (Id-cong () x₁ x₂)

IdℕU-elim : ∀ {Γ l A t u t' u' rU lU} → Γ ⊢ Id ℕ t u ~ Id (Univ rU lU) t' u' ↑! A ^ l → ⊥
IdℕU-elim (Id-cong () x₁ x₂)

IdUUℕ-elim : ∀ {Γ l A t u u'} → Neutral t → Γ ⊢ Id (U ⁰) t u ~ Id (U ⁰) ℕ u' ↑! A ^ l → ⊥
IdUUℕ-elim () (Id-Uℕ x)

IdUUℕ-elim' : ∀ {Γ l A t u u'} → Neutral t → Γ ⊢ Id (U ⁰) ℕ u ~ Id (U ⁰) t u' ↑! A ^ l → ⊥
IdUUℕ-elim' () (Id-Uℕ x)

IdUUΠ-elim- : ∀ {Γ l A rA B X t} → Neutral t → Γ ⊢ t [conv↓] Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰ ∷ X ^ l → ⊥
IdUUΠ-elim- net (η-eq x x₁ x₂ x₃ x₄ x₅ (ne ()) x₇)

IdUUΠ-elim : ∀ {Γ l A rA B X t u u'} → Neutral t → Γ ⊢ Id (U ⁰) t u ~ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) u' ↑! X ^ l → ⊥
IdUUΠ-elim net (Id-cong x y x₂) = let e = conv↑-inversion Uₙ (ne net) Πₙ y in IdUUΠ-elim- net e
IdUUΠ-elim net (Id-U () x₁)
IdUUΠ-elim () (Id-UΠ x x₁)

IdUUΠ-elim' : ∀ {Γ l A rA B X t u u'} → Neutral t → Γ ⊢ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) u ~ Id (U ⁰) t u' ↑! X ^ l → ⊥
IdUUΠ-elim' net e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in IdUUΠ-elim net e'

IdUUΠℕ-elim- : ∀ {Γ l A rA B X} → Γ ⊢ Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰ [conv↓] ℕ ∷ X ^ l → ⊥
IdUUΠℕ-elim- (η-eq x x₁ x₂ x₃ x₄ x₅ (ne ()) x₇)

IdUUΠℕ-elim : ∀ {Γ l A rA B X u u'} → Γ ⊢ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) u ~ Id (U ⁰) ℕ u' ↑! X ^ l → ⊥
IdUUΠℕ-elim (Id-cong x y x₂) = let e = conv↑-inversion Uₙ Πₙ ℕₙ y in IdUUΠℕ-elim- e
IdUUΠℕ-elim (Id-U () x₁)

IdUUΠℕ-elim' : ∀ {Γ l A rA B X u u'} → Γ ⊢ Id (U ⁰) ℕ u ~ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) u' ↑! X ^ l → ⊥
IdUUΠℕ-elim' e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in IdUUΠℕ-elim e'

castℕ-elim : ∀ {Γ l A B B' X t e t' e'} → Neutral A → Γ ⊢ cast ⁰ A B e t ~ cast ⁰ ℕ B' e' t' ↑! X ^ l → ⊥
castℕ-elim neA (cast-cong () x₁ x₂ x₃ x₄)
castℕ-elim () (cast-ℕ x x₁ x₂ x₃)
castℕ-elim () (cast-ℕℕ x x₁ x₂)
castℕ-elim () (cast-ℕΠ x x₁ x₂ x₃)

castℕ-elim' : ∀ {Γ l A B B' X t e t' e'} → Neutral A → Γ ⊢ cast ⁰ ℕ B e t ~ cast ⁰ A B' e' t' ↑! X ^ l → ⊥
castℕ-elim' neA e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in castℕ-elim neA e'

castΠ-elim : ∀ {Γ l A B B' X t e t' e' r P Q} → Neutral A → Γ ⊢ cast ⁰ A B e t ~ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) B' e' t' ↑! X ^ l → ⊥
castΠ-elim neA (cast-cong () x₁ x₂ x₃ x₄)
castΠ-elim () (cast-Π x x₁ x₂ x₃ x₄)
castΠ-elim () (cast-Πℕ x x₁ x₂ x₃)
castΠ-elim () (cast-ΠΠ%! x x₁ x₂ x₃ x₄)
castΠ-elim () (cast-ΠΠ!% x x₁ x₂ x₃ x₄)

castΠ-elim' : ∀ {Γ l A B B' X t e t' e' r P Q} → Neutral A → Γ ⊢ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) B e t ~ cast ⁰ A B' e' t' ↑! X ^ l → ⊥
castΠ-elim' neA e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in castΠ-elim neA e'

castℕℕ-elim : ∀ {Γ l A X t e t' e'} → Neutral A → Γ ⊢ cast ⁰ ℕ A e t ~ cast ⁰ ℕ ℕ e' t' ↑! X ^ l → ⊥
castℕℕ-elim neA (cast-cong () x₁ x₂ x₃ x₄)
castℕℕ-elim (var n) (cast-ℕ () x₁ x₂ x₃)
castℕℕ-elim () (cast-ℕℕ x x₁ x₂)

castℕℕ-elim' : ∀ {Γ l A X t e t' e'} → Neutral A → Γ ⊢ cast ⁰ ℕ ℕ e t ~ cast ⁰ ℕ A e' t' ↑! X ^ l → ⊥
castℕℕ-elim' neA e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in castℕℕ-elim neA e'

castℕΠ-elim : ∀ {Γ l A A' X t e t' e' r P Q} → Γ ⊢ cast ⁰ ℕ A e t ~ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) A' e' t' ↑! X ^ l → ⊥
castℕΠ-elim (cast-cong () x₁ x₂ x₃ x₄)

castℕΠ-elim' : ∀ {Γ l A A' X t e t' e' r P Q} → Γ ⊢ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) A e t ~ cast ⁰ ℕ A' e' t' ↑! X ^ l → ⊥
castℕΠ-elim' (cast-cong () x₁ x₂ x₃ x₄)

castℕneΠ-elim : ∀ {Γ l A X t e t' e' r P Q} → Neutral A → Γ ⊢ cast ⁰ ℕ A e t ~ cast ⁰ ℕ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) e' t' ↑! X ^ l → ⊥
castℕneΠ-elim neA (cast-cong () x₁ x₂ x₃ x₄)
castℕneΠ-elim neA (cast-ℕ () x₁ x₂ x₃)
castℕneΠ-elim () (cast-ℕΠ x x₁ x₂ x₃)

castℕneΠ-elim' : ∀ {Γ l A X t e t' e' r P Q} → Neutral A → Γ ⊢ cast ⁰ ℕ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) e t ~ cast ⁰ ℕ A e' t' ↑! X ^ l → ⊥
castℕneΠ-elim' neA e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in castℕneΠ-elim neA e'

castℕℕΠ-elim : ∀ {Γ l X t e t' e' r P Q} → Γ ⊢ cast ⁰ ℕ ℕ e t ~ cast ⁰ ℕ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) e' t' ↑! X ^ l → ⊥
castℕℕΠ-elim (cast-cong () x₁ x₂ x₃ x₄)
castℕℕΠ-elim (cast-ℕ () x₁ x₂ x₃)

castℕℕΠ-elim' : ∀ {Γ l X t e t' e' r P Q} → Γ ⊢ cast ⁰ ℕ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) e t ~ cast ⁰ ℕ ℕ e' t' ↑! X ^ l → ⊥
castℕℕΠ-elim' e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in castℕℕΠ-elim e'

castΠneℕ-elim : ∀ {Γ l A X t e t' e' r P Q r' P' Q'} → Neutral A → Γ ⊢ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) A e t ~
                                                                       cast ⁰ (Π P' ^ r' ° ⁰ ▹ Q' ° ⁰ ° ⁰) ℕ e' t' ↑! X ^ l → ⊥
castΠneℕ-elim neA (cast-cong () x₁ x₂ x₃ x₄)
castΠneℕ-elim neA (cast-Π x () x₂ x₃ x₄)
castΠneℕ-elim () (cast-Πℕ x x₁ x₂ x₃)

castΠneℕ-elim' : ∀ {Γ l A X t e t' e' r P Q r' P' Q'} → Neutral A → Γ ⊢ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) ℕ e t ~
                                                                       cast ⁰ (Π P' ^ r' ° ⁰ ▹ Q' ° ⁰ ° ⁰) A e' t' ↑! X ^ l → ⊥
castΠneℕ-elim' neA e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in castΠneℕ-elim neA e'

castΠneΠ-elim : ∀ {Γ l A X t e t' e' r P Q r' P' Q' r'' P'' Q''} → Neutral A →
                  Γ ⊢ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) A e t ~ cast ⁰ (Π P' ^ r' ° ⁰ ▹ Q' ° ⁰ ° ⁰) (Π P'' ^ r'' ° ⁰ ▹ Q'' ° ⁰ ° ⁰) e' t' ↑! X ^ l → ⊥
castΠneΠ-elim neA (cast-cong () x₁ x₂ x₃ x₄)
castΠneΠ-elim neA (cast-Π x () x₂ x₃ x₄)
castΠneΠ-elim () (cast-ΠΠ%! x x₁ x₂ x₃ x₄)
castΠneΠ-elim () (cast-ΠΠ!% x x₁ x₂ x₃ x₄)

castΠneΠ-elim' : ∀ {Γ l A X t e t' e' r P Q r' P' Q' r'' P'' Q''} → Neutral A →
                  Γ ⊢ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) (Π P'' ^ r'' ° ⁰ ▹ Q'' ° ⁰ ° ⁰) e t ~ cast ⁰ (Π P' ^ r' ° ⁰ ▹ Q' ° ⁰ ° ⁰) A e' t' ↑! X ^ l → ⊥
castΠneΠ-elim' neA e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in castΠneΠ-elim neA e'

castΠΠℕ-elim : ∀ {Γ l X t e t' e' r P Q r' P' Q' r'' P'' Q''} →
                  Γ ⊢ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) ℕ e t ~ cast ⁰ (Π P' ^ r' ° ⁰ ▹ Q' ° ⁰ ° ⁰) (Π P'' ^ r'' ° ⁰ ▹ Q'' ° ⁰ ° ⁰) e' t' ↑! X ^ l → ⊥
castΠΠℕ-elim (cast-cong () x₁ x₂ x₃ x₄)
castΠΠℕ-elim (cast-Π x () x₂ x₃ x₄)

castΠΠℕ-elim' : ∀ {Γ l X t e t' e' r P Q r' P' Q' r'' P'' Q''} →
                  Γ ⊢ cast ⁰ (Π P ^ r ° ⁰ ▹ Q ° ⁰ ° ⁰) (Π P'' ^ r'' ° ⁰ ▹ Q'' ° ⁰ ° ⁰) e t ~ cast ⁰ (Π P' ^ r' ° ⁰ ▹ Q' ° ⁰ ° ⁰) ℕ e' t' ↑! X ^ l → ⊥
castΠΠℕ-elim' e = let _ , _ , e' = sym~↑! (reflConEq (wfEqTerm (soundness~↑! e))) e in castΠΠℕ-elim e'

castΠΠ!%-elim : ∀ {Γ l A A' X t e t' e' P Q P' Q'} → Γ ⊢ cast ⁰ (Π P ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰) A e t ~
                                                         cast ⁰ (Π P' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰) A' e' t' ↑! X ^ l → ⊥
castΠΠ!%-elim (cast-cong () x₁ x₂ x₃ x₄)

castΠΠ%!-elim : ∀ {Γ l A A' X t e t' e' P Q P' Q'} → Γ ⊢ cast ⁰ (Π P ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰) A e t ~
                                                         cast ⁰ (Π P' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰) A' e' t' ↑! X ^ l → ⊥
castΠΠ%!-elim (cast-cong () x₁ x₂ x₃ x₄)

  -- Helper functions for decidability for neutrals
decConv↓Term-ℕ-ins : ∀ {t u Γ l}
 → Γ ⊢ t [conv↓] u ∷ ℕ ^ l
 → Γ ⊢ t ~ t ↓! ℕ ^ l
 → Γ ⊢ t ~ u ↓! ℕ ^ l
decConv↓Term-ℕ-ins (ℕ-ins x) t~t = x
decConv↓Term-ℕ-ins (ne-ins x x₁ () x₃) t~t
decConv↓Term-ℕ-ins (zero-refl x) ([~] A D whnfB ())
decConv↓Term-ℕ-ins (suc-cong x) ([~] A D whnfB ())

decConv↓Term-U-ins : ∀ {t u Γ r lU l}
  → Γ ⊢ t [conv↓] u ∷ Univ r lU ^ l
  → Γ ⊢ t ~ t ↓! Univ r lU ^ l
  → Γ ⊢ t ~ u ↓! Univ r lU ^ l
decConv↓Term-U-ins (ne x) t~r = x

decConv↓Term-ne-ins : ∀ {t u A Γ l}
  → Neutral A
  → Γ ⊢ t [conv↓] u ∷ A ^ l
  → ∃ λ B → ∃ λ lB → Γ ⊢ t ~ u ↓! B ^ lB
decConv↓Term-ne-ins neA (ne-ins x x₁ x₂ x₃) = _ , _ , x₃

-- Helper function for decidability for impossibility of terms not being equal
-- as neutrals when they are equal as terms and the first is a neutral.
decConv↓Term-ℕ : ∀ {t u Γ l}
  → Γ ⊢ t [conv↓] u ∷ ℕ ^ l
  → Γ ⊢ t ~ t ↓! ℕ ^ l
  → ¬ (Γ ⊢ t ~ u ↓! ℕ ^ l)
  → ⊥
decConv↓Term-ℕ (ℕ-ins x) t~t ¬u~u = ¬u~u x
decConv↓Term-ℕ (ne-ins x x₁ () x₃) t~t ¬u~u
decConv↓Term-ℕ (zero-refl x) ([~] A D whnfB ()) ¬u~u
decConv↓Term-ℕ (suc-cong x) ([~] A D whnfB ()) ¬u~u

decConv↓Term-U : ∀ {t u Γ r lU l}
  → Γ ⊢ t [conv↓] u ∷ Univ r lU ^ l
  → Γ ⊢ t ~ t ↓! Univ r lU ^ l
  → ¬ (Γ ⊢ t ~ u ↓! Univ r lU ^ l)
  → ⊥
decConv↓Term-U (ne x) t~t ¬u~u = ¬u~u x


text:
record R (X : Set) : Set₁ where
  field
    P : X → Set
    f : ∀ {x : X} → P x → P x

open R {{…}}

test : ∀ {X} {{r : R X}} {x : X} → P x → P x
test p = f p

-- WAS: instance search fails with several candidates left
-- SHOULD: succeed