ial/closures.agda at master · cedille/ial · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
open import bool
open import level
open import eq
open import product
open import product-thms
open import relations

module closures where

  module basics {ℓ : level}{A : Set ℓ} (_>A_ : A → A → Set ℓ) where

    data tc : A → A → Set ℓ where
      tc-step : ∀{a b : A} → a >A b → tc a b
      tc-trans : ∀{a b c : A} → tc a b → tc b c → tc a c

    data rc : A → A → Set ℓ where
      rc-step : ∀{a b : A} → a >A b → rc a b
      rc-refl : ∀{a : A} → rc a a

    tc-transitive : transitive tc
    tc-transitive = tc-trans

  module combinations {ℓ : level}{A : Set ℓ} (_>A_ : A → A → Set ℓ) where
     open basics public

     rtc : A → A → Set ℓ
     rtc = rc (tc _>A_)

     rtc-refl : reflexive rtc
     rtc-refl = rc-refl

     rtc-trans : transitive rtc
     rtc-trans (rc-step{a}{b} x) (rc-step{.b}{c} x') = rc-step (tc-trans x x')
     rtc-trans (rc-step x) rc-refl = rc-step x
     rtc-trans rc-refl (rc-step x) = rc-step x
     rtc-trans rc-refl rc-refl = rc-refl