| 12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273 |
- module DefinitionalEquality where
- postulate
- _≡_ : {A B : Set} -> A -> B -> Set
- refl-≡ : {A : Set}{x : A} -> x ≡ x
- subst-≡ : {A : Set}{x y : A}(C : A -> Set) -> x ≡ y -> C y -> C x
- subst-≡¹ : {A : Set}{x y : A}(C : A -> Set1) -> x ≡ y -> C y -> C x
- subst-≡' : {A B : Set}{x : A}{y : B}(C : {X : Set} -> X -> Set) -> x ≡ y -> C y -> C x
- app-≡₀ : {A₁ A₂ : Set}{B₁ : A₁ -> Set}{B₂ : A₂ -> Set}
- {f : (x : A₁) -> B₁ x}{g : (x : A₂) -> B₂ x}{a₁ : A₁}{a₂ : A₂} ->
- f ≡ g -> a₁ ≡ a₂ -> f a₁ ≡ g a₂
- η-≡ : {A₁ A₂ : Set}{B₁ : A₁ -> Set}{B₂ : A₂ -> Set}
- {f₁ : (x : A₁) -> B₁ x}{f₂ : (x : A₂) -> B₂ x} ->
- ((x : A₁)(y : A₂) -> x ≡ y -> f₁ x ≡ f₂ y) -> f₁ ≡ f₂
- -- Substitution is a no-op
- subst-≡-identity : {A : Set}{x y : A}(C : A -> Set)(p : x ≡ y)(cy : C y) ->
- subst-≡ C p cy ≡ cy
- cong-≡ : {A B : Set}{x y : A}(f : A -> B)(p : x ≡ y) -> f x ≡ f y
- cong-≡ {_}{_}{_}{y} f p = subst-≡ (\z -> f z ≡ f y) p refl-≡
- cong-≡' : {A : Set}{B : A -> Set}{x y : A}(f : (z : A) -> B z)(p : x ≡ y) -> f x ≡ f y
- cong-≡' {_}{_}{_}{y} f p = subst-≡ (\z -> f z ≡ f y) p refl-≡
- cong₂-≡' : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
- {x y : A}{z : B x}{w : B y}(f : (x : A)(z : B x) -> C x z) ->
- x ≡ y -> z ≡ w -> f x z ≡ f y w
- cong₂-≡' f xy zw = app-≡₀ (cong-≡' f xy) zw
- trans-≡ : {A B C : Set}(x : A)(y : B)(z : C) -> x ≡ y -> y ≡ z -> x ≡ z
- trans-≡ x y z xy yz = subst-≡' (\w -> w ≡ z) xy yz
- postulate
- _≡₁_ : {A B : Set1} -> A -> B -> Set1
- refl-≡₁ : {A : Set1}{x : A} -> x ≡₁ x
- subst-≡₁ : {A : Set1}{x y : A}(C : A -> Set1) -> x ≡₁ y -> C y -> C x
- subst-≡₁' : {A B : Set1}{x : A}{y : B}(C : {X : Set1} -> X -> Set1) -> x ≡₁ y -> C y -> C x
- -- Substitution is a no-op
- subst-≡₁-identity : {A : Set1}{x y : A}(C : A -> Set1)(p : x ≡₁ y)(cy : C y) ->
- subst-≡₁ C p cy ≡₁ cy
- app-≡₁ : {A₁ A₂ : Set1}{B₁ : A₁ -> Set1}{B₂ : A₂ -> Set1}
- {f : (x : A₁) -> B₁ x}{g : (x : A₂) -> B₂ x}{a₁ : A₁}{a₂ : A₂} ->
- f ≡₁ g -> a₁ ≡₁ a₂ -> f a₁ ≡₁ g a₂
- app-≡₁⁰ : {A₁ A₂ : Set}{B₁ : A₁ -> Set1}{B₂ : A₂ -> Set1}
- {f : (x : A₁) -> B₁ x}{g : (x : A₂) -> B₂ x}{a₁ : A₁}{a₂ : A₂} ->
- f ≡₁ g -> a₁ ≡ a₂ -> f a₁ ≡₁ g a₂
- η-≡₁ : {A₁ A₂ : Set1}{B₁ : A₁ -> Set1}{B₂ : A₂ -> Set1}
- {f₁ : (x : A₁) -> B₁ x}{f₂ : (x : A₂) -> B₂ x} ->
- ((x : A₁)(y : A₂) -> x ≡₁ y -> f₁ x ≡₁ f₂ y) -> f₁ ≡₁ f₂
- η-≡₁⁰ : {A₁ A₂ : Set}{B₁ : A₁ -> Set1}{B₂ : A₂ -> Set1}
- {f₁ : (x : A₁) -> B₁ x}{f₂ : (x : A₂) -> B₂ x} ->
- ((x : A₁)(y : A₂) -> x ≡ y -> f₁ x ≡₁ f₂ y) -> f₁ ≡₁ f₂
- cong-≡₁ : {A B : Set1}{x y : A}(f : A -> B)(p : x ≡₁ y) -> f x ≡₁ f y
- cong-≡₁ {_}{_}{_}{y} f p = subst-≡₁ (\z -> f z ≡₁ f y) p refl-≡₁
- cong-≡₁⁰ : {A : Set}{B : A -> Set1}{x y : A}(f : (x : A) -> B x)(p : x ≡ y) -> f x ≡₁ f y
- cong-≡₁⁰ {_}{_}{_}{y} f p = subst-≡¹ (\z -> f z ≡₁ f y) p refl-≡₁
- trans-≡₁ : {A B C : Set1}(x : A)(y : B)(z : C) -> x ≡₁ y -> y ≡₁ z -> x ≡₁ z
- trans-≡₁ x y z xy yz = subst-≡₁' (\w -> w ≡₁ z) xy yz
|
