fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Rename some variables

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2017-11-15 21:59:00 +01:00
parent 43cc73c6a8
commit 11f5b89b10
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Category/Rel.agda
View file

@ -22,7 +22,7 @@ Subset A = A → Set
-- syntax subset P = ⦃ a ∈ A | P a ⦄ -- syntax subset P = ⦃ a ∈ A | P a ⦄
-- syntax subset-syntax A (λ a → B) = ⟨ a foo A ∣ B ⟩ -- syntax subset-syntax A (λ a → B) = ⟨ a foo A ∣ B ⟩
-- Membership is function applicatiom. -- Membership is (dependent) function applicatiom.
_∈_ : {ℓ : Level} {A : Set ℓ} → A → Subset A → Set _∈_ : {ℓ : Level} {A : Set ℓ} → A → Subset A → Set
s ∈ S = S s s ∈ S = S s
@ -30,7 +30,7 @@ infixl 45 _∈_
-- The diagnoal of a set is a synonym for equality. -- The diagnoal of a set is a synonym for equality.
Diag : ∀ S → Subset (S × S) Diag : ∀ S → Subset (S × S)
Diag S (s₀ , s₁) = s₀ ≡ s₁ Diag S (x , y) = x ≡ y
-- Diag S = subset (S × S) (λ {(p , q) → p ≡ q}) -- Diag S = subset (S × S) (λ {(p , q) → p ≡ q})
-- Diag S = ⟨ ? foo ? ∣ ? ⟩ -- Diag S = ⟨ ? foo ? ∣ ? ⟩
-- Diag S (s₀ , s₁) = ⦃ (s₀ , s₁) ∈ S | s₀ ≡ s₁ ⦄ -- Diag S (s₀ , s₁) = ⦃ (s₀ , s₁) ∈ S | s₀ ≡ s₁ ⦄
@ -147,9 +147,9 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
equi = fwd , isequiv equi = fwd , isequiv
-- assocc : Q + (R + S) ≡ (Q + R) + S -- assocc : Q + (R + S) ≡ (Q + R) + S
assocc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) is-assoc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) ≡ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
assocc = equivToPath equi is-assoc = equivToPath equi
Rel : Category Rel : Category
Rel = record Rel = record
@ -157,6 +157,6 @@ Rel = record
; Arrow = λ S R → Subset (S × R) ; Arrow = λ S R → Subset (S × R)
; 𝟙 = λ {S} → Diag S ; 𝟙 = λ {S} → Diag S
; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )} ; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
; assoc = funExt assocc ; assoc = funExt is-assoc
; ident = funExt ident-l , funExt ident-r ; ident = funExt ident-l , funExt ident-r
} }