Taneb
/
thinnings
1
Fork 0
Code Issues 3 Pull Requests Packages Projects Releases Wiki Activity

Initial objects #4

Merged
Taneb merged 3 commits from initial-objects into main 2024-06-20 11:49:46 +01:00
Conversation 0 Commits 3 Files Changed 3 +6 -1
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit a0a743ac71 - Show all commits

7
src/Thinning/Properties.agda
View File

@ -2,7 +2,7 @@
module Thinning.Properties where module Thinning.Properties where
open import Data.List.Base using (List) open import Data.List.Base using (List; [])
open import Level using (Level) open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
@ -48,3 +48,8 @@ assoc (exclude θ) (include φ) (include ψ) = cong exclude (assoc θ φ ψ)
assoc (exclude θ) (include φ) (exclude ψ) = cong exclude (assoc (exclude θ) (include φ) ψ) assoc (exclude θ) (include φ) (exclude ψ) = cong exclude (assoc (exclude θ) (include φ) ψ)
assoc (exclude θ) (exclude φ) (include ψ) = cong exclude (assoc (exclude θ) φ ψ) assoc (exclude θ) (exclude φ) (include ψ) = cong exclude (assoc (exclude θ) φ ψ)
assoc (exclude θ) (exclude φ) (exclude ψ) = cong exclude (assoc (exclude θ) (exclude φ) ψ) assoc (exclude θ) (exclude φ) (exclude ψ) = cong exclude (assoc (exclude θ) (exclude φ) ψ)
-- ¡ is the only Thinning from []
¡-unique : (θ : Thinning A [] xs) → ¡ ≡ θ
¡-unique end = refl
¡-unique (exclude θ) = cong exclude (¡-unique θ)