Dan's 數位πŸͺ΄εœ’

Partial Equivalence Relations

1 min read

misc 
module agda.PER where
open import Level
open import Data.Product
open import Relation.Binary.Core

variable
  a β„“ : Level

record PartialEquivalenceRel {A : Set a} (_~_ : Rel A β„“) : Set (a βŠ” β„“) where
  constructor PER
  field
    sym : {a b : A} β†’ a ~ b β†’ b ~ a
    trans : {a b c : A} β†’ a ~ b β†’ b ~ c β†’ a ~ c

QuasiReflexive : (A : Set a) (_~_ : Rel A β„“) β†’ Set (a βŠ” β„“)
QuasiReflexive A _~_ = βˆ€ {x y : A} β†’ (x ~ y) β†’ (x ~ x) Γ— (y ~ y)

open PartialEquivalenceRel {{...}}

quasi-reflexive : {A : Set a} {x y : A} {_~_ : Rel A β„“} β†’
  {{PartialEquivalenceRel _~_}} β†’ QuasiReflexive A _~_
quasi-reflexive x~y = (trans x~y (sym x~y)) , (trans (sym x~y) x~y)

Graph View

Backlinks