text:
-- Andreas, 2015-09-12, Issue 1637, reported by Nisse.
-- {-# OPTIONS -v tc.display:100 -v reify.display:100 #-}

record R (X : Set₁) : Set₁ where
  field
    f : X

postulate
  A : Set₁
  P : A → Set

module M (_ : Set₁) where

  Unrelated-function : R Set → Set
  Unrelated-function Y = R.f Y  -- eta expansion is necessary

open M Set

  -- Here, the old implementation recursively added a display form
  -- for R.f because the body of Unrelated-function has the right
  -- form, looking as if it came from a module application.

  -- adding display forms
  --   Issue1637.M.Unrelated-function --> Issue1637._.Unrelated-function
  --   Issue1637.R.f --> Issue1637._.Unrelated-function

  -- If one restricts display forms to things that actually
  -- come from a module applications, i.e., are a defCopy,
  -- then this issue is fixed.

Foo : ((Z : R A) → P (R.f Z)) → Set₁
Foo f = f

-- The inferred type of f is (printed as?)
--
--   (Z : R A) → P Unrelated-function,
--
-- which is not a type-correct expression.
--
-- The bug exists in Agda 2.3.2, but not in Agda 2.3.0.1.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Structure.Category.Categories where

open import Data
open import Data.Proofs
open import Functional
open import Logic
import      Lvl
import      Relator.Equals as Eq
open import Structure.Setoid
open import Structure.Category
open import Structure.Categorical.Proofs
open import Structure.Categorical.Properties
open import Structure.Operator
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ : Lvl.Level
private variable Obj A B : Type{ℓ}
private variable _▫_ : Obj → Obj → Type{ℓ}
private variable f : A → B

-- The empty category is a category containing nothing.
-- The objects are empty.
-- The morphisms are empty.
emptyCategory : Category{ℓ₁}{ℓ₂}{ℓₑ}(empty-morphism) ⦃ \{} ⦄
Category._∘_            emptyCategory = empty-comp
Category.id             emptyCategory = empty-id
Category.binaryOperator emptyCategory {}
Category.associativity  emptyCategory = empty-associativity ⦃ \{} ⦄
Category.identity       emptyCategory = empty-identity ⦃ \{} ⦄

-- The single category is a category containing a single object and a single morphism.
-- The objects consists of a single thing.
-- The morphisms consists of a single connection connecting the single thing to itself.
singleCategory : ∀{ℓₒ ℓᵢ ℓₚₐ₁ ℓₚₐ₂ ℓₚᵢ₁ ℓₚᵢ₂ ℓₚᵢ₃ : Lvl.Level} → Category{ℓ₁}{ℓ₂}(single-morphism)
Category._∘_ (singleCategory{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}) = single-comp{ℓ₂}{ℓₒ}
Category.id  (singleCategory{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}) = single-id{ℓ₂}{ℓᵢ}
BinaryOperator.congruence (Category.binaryOperator singleCategory) Eq.[≡]-intro Eq.[≡]-intro = Eq.[≡]-intro
Category.associativity (singleCategory{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}) = single-associativity{ℓ₂}{ℓ₂}{ℓₚₐ₁}{ℓ₁}{ℓₚₐ₂}
Category.identity      (singleCategory{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}) = single-identity{ℓ₂}{ℓ₂}{ℓₚᵢ₁}{ℓ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}

on₂-category : ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}{ℓ}(x ▫ y) ⦄ → Category{Obj = B}(_▫_) ⦃ morphism-equiv ⦄ → (f : A → B) → Category((_▫_) on₂ f)
Category._∘_ (on₂-category C _) = Category._∘_ C
Category.id  (on₂-category C _) = Category.id  C
BinaryOperator.congruence (Category.binaryOperator (on₂-category C _)) = BinaryOperator.congruence(Category.binaryOperator C)
Category.associativity (on₂-category C f) = on₂-associativity f (Category.associativity C)
Category.identity      (on₂-category C f) = on₂-identity f (Category.identity C)

{-
TODO:
• https://en.wikipedia.org/wiki/Isomorphism_of_categories
• https://en.wikipedia.org/wiki/Equivalence_of_categories
?
-}

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 --cubical --no-import-sorts --safe #-}

module Cubical.Relation.Binary.Raw.Definitions where

open import Cubical.Core.Everything

open import Cubical.Foundations.Function
open import Cubical.Data.Maybe.Base using (Maybe)
open import Cubical.Data.Prod.Base using (_×_)
open import Cubical.Data.Sigma.Base using (∃-syntax)
open import Cubical.Data.Sum.Base using (_⊎_)
open import Cubical.HITs.PropositionalTruncation.Base using (∥_∥)

open import Cubical.Relation.Binary.Base
open import Cubical.Relation.Nullary.Decidable

private
  variable
    a b c ℓ ℓ′ ℓ′′ : Level
    A : Type a
    B : Type b
    C : Type c

infix 8 _⟶_Respects_ _Respects_ _Respectsˡ_ _Respectsʳ_ _Respects₂_

------------------------------------------------------------------------
-- Basic definitions
------------------------------------------------------------------------

idRel : (A : Type ℓ) → RawRel A ℓ
idRel A a b = a ≡ b

invRel : ∀ {A B : Type ℓ} → RawREL A B ℓ′ → RawREL B A ℓ′
invRel R b a = R a b

compRel : ∀ {A B C : Type ℓ} → RawREL A B ℓ′ → RawREL B C ℓ′′ → RawREL A C _
compRel R S a c = Σ[ b ∈ _ ] (R a b × S b c)

graphRel : ∀ {A B : Type ℓ} → (A → B) → RawREL A B ℓ
graphRel f a b = f a ≡ b

infix 7 _⇒_ _⇔_ _=[_]⇒_

-- Implication/containment - could also be written _⊆_.
-- and corresponding notion of equivalence

_⇒_ : RawREL A B ℓ → RawREL A B ℓ′ → Type _
P ⇒ Q = ∀ {x y} → P x y → Q x y

_⇔_ : RawREL A B ℓ → RawREL A B ℓ′ → Type _
P ⇔ Q = P ⇒ Q × Q ⇒ P

-- Generalised implication - if P ≡ Q it can be read as "f preserves P".

_=[_]⇒_ : RawRel A ℓ → (A → B) → RawRel B ℓ′ → Type _
P =[ f ]⇒ Q = P ⇒ (Q on f)

-- A synonym for _=[_]⇒_.

_Preserves_⟶_ : (A → B) → RawRel A ℓ → RawRel B ℓ′ → Type _
f Preserves P ⟶ Q = P =[ f ]⇒ Q

-- An endomorphic variant of _Preserves_⟶_.

_Preserves_ : (A → A) → RawRel A ℓ → Type _
f Preserves P = f Preserves P ⟶ P

-- A binary variant of _Preserves_⟶_.

_Preserves₂_⟶_⟶_ : (A → B → C) → RawRel A ℓ → RawRel B ℓ′ → RawRel C ℓ′′ → Type _
_∙_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y u v} → P x y → Q u v → R (x ∙ u) (y ∙ v)

------------------------------------------------------------------------
-- Property predicates
------------------------------------------------------------------------

-- Reflexivity.

Reflexive : RawRel A ℓ → Type _
Reflexive _∼_ = ∀ {x} → x ∼ x

-- Equality can be converted to proof of relation.

FromEq : RawRel A ℓ → Type _
FromEq _∼_ = _≡_ ⇒ _∼_

-- Irreflexivity.

Irreflexive : RawRel A ℓ → Type _
Irreflexive _<_ = ∀ {x} → ¬ (x < x)

-- Relation implies inequality.

ToNotEq : RawRel A ℓ → Type _
ToNotEq _<_ = _<_ ⇒ (λ x y → ¬ (x ≡ y))

-- Generalised symmetry.

Sym : RawREL A B ℓ → RawREL B A ℓ′ → Type _
Sym P Q = P ⇒ flip Q

-- Symmetry.

Symmetric : RawRel A ℓ → Type _
Symmetric _∼_ = Sym _∼_ _∼_

-- Generalised transitivity.

Trans : RawREL A B ℓ → RawREL B C ℓ′ → RawREL A C ℓ′′ → Type _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k

-- A flipped variant of generalised transitivity.

TransFlip : RawREL A B ℓ → RawREL B C ℓ′ → RawREL A C ℓ′′ → Type _
TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k

-- Transitivity.

Transitive : RawRel A ℓ → Type _
Transitive _∼_ = Trans _∼_ _∼_ _∼_

-- Generalised antisymmetry.

Antisym : RawREL A B ℓ → RawREL B A ℓ′ → RawREL A B ℓ′′ → Type _
Antisym R S E = ∀ {i j} → R i j → S j i → E i j

-- Antisymmetry.

Antisymmetric : RawRel A ℓ → Type _
Antisymmetric _≤_ = Antisym _≤_ _≤_ _≡_

-- Asymmetry.

Asymmetric : RawRel A ℓ → Type _
Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)

-- Generalised connex - exactly one of the two relations holds.

Connex : RawREL A B ℓ → RawREL B A ℓ′ → Type _
Connex P Q = ∀ x y → P x y ⊎ Q y x

-- Totality.

Total : RawRel A ℓ → Type _
Total _∼_ = Connex _∼_ _∼_

-- Truncated connex - Preserves propositions.

PropConnex : RawREL A B ℓ → RawREL B A ℓ′ → Type _
PropConnex P Q = ∀ x y → ∥ P x y ⊎ Q y x ∥

-- Truncated totality.

PropTotal : RawRel A ℓ → Type _
PropTotal _∼_ = PropConnex _∼_ _∼_

-- Generalised trichotomy - exactly one of three types has a witness.

data Tri (A : Type a) (B : Type b) (C : Type c) : Type (ℓ-max a (ℓ-max b c)) where
  tri< : ( a :   A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
  tri≡ : (¬a : ¬ A) ( b :   B) (¬c : ¬ C) → Tri A B C
  tri> : (¬a : ¬ A) (¬b : ¬ B) ( c :   C) → Tri A B C

-- Trichotomy.

Trichotomous : RawRel A ℓ → Type _
Trichotomous _<_ = ∀ x y → Tri (x < y) (x ≡ y) (x > y)
  where _>_ = flip _<_

-- Generalised maximum element.

Max : RawREL A B ℓ → B → Type _
Max _≤_ T = ∀ x → x ≤ T

-- Maximum element.

Maximum : RawRel A ℓ → A → Type _
Maximum = Max

-- Generalised minimum element.

Min : RawREL A B ℓ → A → Type _
Min R = Max (flip R)

-- Minimum element.

Minimum : RawRel A ℓ → A → Type _
Minimum = Min

-- Unary relations respecting a binary relation.

_⟶_Respects_ : (A → Type ℓ) → (B → Type ℓ′) → RawREL A B ℓ′′ → Type _
P ⟶ Q Respects _∼_ = ∀ {x y} → x ∼ y → P x → Q y

-- Unary relation respects a binary relation.

_Respects_ : (A → Type ℓ) → RawRel A ℓ′ → Type _
P Respects _∼_ = P ⟶ P Respects _∼_

-- Right respecting - relatedness is preserved on the right by some equivalence.

_Respectsʳ_ : RawREL A B ℓ → RawRel B ℓ′ → Type _
_∼_ Respectsʳ _≈_ = ∀ {x} → (x ∼_) Respects _≈_

-- Left respecting - relatedness is preserved on the left by some equivalence.

_Respectsˡ_ : RawREL A B ℓ → RawRel A ℓ′ → Type _
_∼_ Respectsˡ _≈_ = ∀ {y} → (_∼ y) Respects _≈_

-- Respecting - relatedness is preserved on both sides by some equivalence.

_Respects₂_ : RawRel A ℓ → RawRel A ℓ′ → Type _
_∼_ Respects₂ _≈_ = (_∼_ Respectsʳ _≈_) × (_∼_ Respectsˡ _≈_)

-- Substitutivity - any two related elements satisfy exactly the same
-- set of unary relations. Note that only the various derivatives
-- of propositional equality can satisfy this property.

Substitutive : RawRel A ℓ → (ℓ′ : Level) → Type _
Substitutive {A = A} _∼_ p = (P : A → Type p) → P Respects _∼_

-- Decidability - it is possible to determine whether a given pair of
-- elements are related.

Decidable : RawREL A B ℓ → Type _
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

-- Weak decidability - it is sometimes possible to determine if a given
-- pair of elements are related.

WeaklyDecidable : RawREL A B ℓ → Type _
WeaklyDecidable _∼_ = ∀ x y → Maybe (x ∼ y)

-- Universal - all pairs of elements are related

Universal : RawREL A B ℓ → Type _
Universal _∼_ = ∀ x y → x ∼ y

-- Non-emptiness - at least one pair of elements are related.

NonEmpty : RawREL A B ℓ → Type _
NonEmpty _∼_ = ∃[ x ∈ _ ] ∃[ y ∈ _ ] x ∼ y


text:
module logic where

open import Level
open import Relation.Nullary
open import Relation.Binary hiding (_⇔_ )
open import Data.Empty

data Bool : Set where
    true : Bool
    false : Bool

record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   constructor ⟪_,_⟫
   field
      proj1 : A
      proj2 : B

data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   case1 : A → A ∨ B
   case2 : B → A ∨ B

_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
_⇔_ A B =  ( A → B ) ∧ ( B → A )

contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )

double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
double-neg A notnot = notnot A

double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
double-neg2 notnot A = notnot ( double-neg A )

de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))

dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
dont-or {A} {B} (case2 b) ¬A = b

dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
dont-orb {A} {B} (case1 a) ¬B = a

infixr  130 _∧_
infixr  140 _∨_
infixr  150 _⇔_

_/\_ : Bool → Bool → Bool
true /\ true = true
_ /\ _ = false

_\/_ : Bool → Bool → Bool
false \/ false = false
_ \/ _ = true

not_ : Bool → Bool
not true = false
not false = true

_<=>_ : Bool → Bool → Bool
true <=> true = true
false <=> false = true
_ <=> _ = false

infixr  130 _\/_
infixr  140 _/\_

open import Relation.Binary.PropositionalEquality

≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
≡-Bool-func {true} {true} a→b b→a = refl
≡-Bool-func {false} {true} a→b b→a with b→a refl
... | ()
≡-Bool-func {true} {false} a→b b→a with a→b refl
... | ()
≡-Bool-func {false} {false} a→b b→a = refl

bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
bool-≡-? true true = yes refl
bool-≡-? true false = no (λ ())
bool-≡-? false true = no (λ ())
bool-≡-? false false = yes refl

¬-bool-t : {a : Bool} →  ¬ ( a ≡ true ) → a ≡ false
¬-bool-t {true} ne = ⊥-elim ( ne refl )
¬-bool-t {false} ne = refl

¬-bool-f : {a : Bool} →  ¬ ( a ≡ false ) → a ≡ true
¬-bool-f {true} ne = refl
¬-bool-f {false} ne = ⊥-elim ( ne refl )

¬-bool : {a : Bool} →  a ≡ false  → a ≡ true → ⊥
¬-bool refl ()

lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
lemma-∧-0 {true} {true} refl ()
lemma-∧-0 {true} {false} ()
lemma-∧-0 {false} {true} ()
lemma-∧-0 {false} {false} ()

lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
lemma-∧-1 {true} {true} refl ()
lemma-∧-1 {true} {false} ()
lemma-∧-1 {false} {true} ()
lemma-∧-1 {false} {false} ()

bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
bool-and-tt refl refl = refl

bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true
bool-∧→tt-0 {true} {true} refl = refl
bool-∧→tt-0 {false} {_} ()

bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true
bool-∧→tt-1 {true} {true} refl = refl
bool-∧→tt-1 {true} {false} ()
bool-∧→tt-1 {false} {false} ()

bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b
bool-or-1 {false} {true} refl = refl
bool-or-1 {false} {false} refl = refl
bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a
bool-or-2 {true} {false} refl = refl
bool-or-2 {false} {false} refl = refl

bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true
bool-or-3 {true} = refl
bool-or-3 {false} = refl

bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true
bool-or-31 {true} {true} refl = refl
bool-or-31 {false} {true} refl = refl

bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true
bool-or-4 {true} = refl
bool-or-4 {false} = refl

bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true
bool-or-41 {true} {b} refl = refl

bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
bool-and-1 {false} {b} refl = refl
bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
bool-and-2 {true} {false} refl = refl
bool-and-2 {false} {false} refl = refl

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
module Oscar.Class.Reflexivity where

open import Oscar.Level

record Reflexivity {a} {A : Set a} {ℓ} (_≋_ : A → A → Set ℓ) : Set (a ⊔ ℓ) where
  field
    reflexivity : ∀ {x} → x ≋ x

open Reflexivity ⦃ … ⦄ public