Deprecated : The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Prelude module Prelude where
open import Agda.Primitive public
record LiftSet { l l' : Level } ( A : Set l ) : Set ( l ⊔ l' ) where
constructor ↑set
field ↓set : A
open LiftSet public
record LiftProp { l l' : Level } ( P : Prop l ) : Set ( l ⊔ l' ) where
constructor ↑prop
field ↓prop : P
open LiftProp public
id :
{ l : Level }
{ A : Set l }
→
A → A
id x = x
K :
{ l m : Level }
{ A : Set l }
( B : Set m )
→
A → B → A
K _ x _ = x
infixr 5 _∘_
_∘_ :
{ l m n : Level }
{ A : Set l }
{ B : A → Set m }
{ C : ( x : A ) → B x → Set n }
( g : { x : A }( y : B x ) → C x y )
( f : ( x : A ) → B x )
→
( x : A ) → C x ( f x )
( g ∘ f ) x = g ( f x )
data 𝟘 { l : Level } : Set l where
𝟘e :
{ l m : Level }
{ A : 𝟘 { l } → Set m }
→
∀ x → A x
𝟘e ()
data 𝔹 : Set where
true false : 𝔹
{-# BUILTIN BOOL 𝔹 #-}
{-# BUILTIN TRUE true #-}
{-# BUILTIN FALSE false #-}
data ⊤ { l : Level } : Prop l where
⊤i : ⊤
data ⊥ { l : Level } : Prop l where
infix 3 ¬_
¬_ : { l : Level } → Prop l → Prop l
¬_ { l } P = P → ⊥ { l }
infix 4 _===_
data _===_
{ l : Level }
{ A : Set l }
:
{ B : Set l }( x : A )( y : B ) → Prop l
where
instance refl : { x : A } → x === x
{-# BUILTIN REWRITE _===_ #-}
===irrel :
{ l : Level }
{ P Q : Prop l }
{ p : P }
{ q : Q }
→
P === Q → ↑prop { l }{ l } p === ↑prop q
===irrel refl = refl
===typ :
{ l : Level }
{ A B : Set l }
{ x : A }
{ y : B }
→
x === y → A === B
===typ refl = refl
coeₚ : { l : Level }{ P Q : Prop l } → P === Q → P → Q
coeₚ refl x = x
coeₚ⁻¹ : { l : Level }{ P Q : Prop l } → P === Q → Q → P
coeₚ⁻¹ refl x = x
ap :
{ l m : Level }
{ A : Set l }
{ B : A → Set m }
( f : ( x : A ) → B x )
{ x y : A }
( _ : x === y )
→
f x === f y
ap _ refl = refl
ap₂ :
{ l m n : Level }
{ A : Set l }
{ B : A → Set m }
{ C : ( x : A ) → B x → Set n }
( f : ( x : A )( y : B x ) → C x y )
{ x x' : A }
( _ : x === x' )
{ y : B x }
{ y' : B x' }
( _ : y === y' )
→
f x y === f x' y'
ap₂ _ refl refl = refl
trans :
{ l : Level }
{ A B C : Set l }
{ x : A }
{ y : B }
{ z : C }
( q : y === z )
( p : x === y )
→
x === z
trans refl p = p
symm :
{ l : Level }
{ A B : Set l }
{ x : A }
{ y : B }
( p : x === y )
→
y === x
symm refl = refl
infix 1 proof_
proof_ :
{ l : Level }
{ A B : Set l }
{ x : A }
{ y : B }
→
x === y → x === y
proof p = p
infixr 2 _=[_]_
_=[_]_ :
{ l : Level }
{ A B C : Set l }
( x : A )
{ y : B }
{ z : C }
→
x === y → y === z → x === z
_ =[ p ] q = trans q p
infix 3 _qed
_qed :
{ l : Level }
{ A : Set l }
( x : A )
→
x === x
_ qed = refl
substp :
{ l m : Level }
{ A A' : Set l }
{ P : A → Prop m }
{ P' : A' → Prop m }
( _ : P === P' )
{ x : A }
{ x' : A' }
( _ : x === x' )
→
P x → P' x'
substp e e' p with ===typ e'
substp refl refl p | refl = p
substp₂ :
{ l m n : Level }
{ A A' : Set l }
{ B B' : Set m }
{ P : A → B → Prop n }
{ P' : A' → B' → Prop n }
( _ : P === P' )
{ x : A }
{ x' : A' }
{ y : B }
{ y' : B' }
( _ : x === x' )
( _ : y === y' )
→
P x y → P' x' y'
substp₂ e e' e'' p with ===typ e' | ===typ e''
substp₂ refl refl refl p | refl | refl = p
infix 4 _==_
_==_ : { l : Level }{ A : Set l }( x y : A ) → Prop l
_==_ = _===_
infixr 3 _∧_
data _∧_ { l m : Level }( P : Prop l )( Q : Prop m ) : Prop ( l ⊔ m ) where
∧i : P → Q → P ∧ Q
∧e₁ :
{ l m : Level }
{ P : Prop l }
{ Q : Prop m }
→
P ∧ Q → P
∧e₁ ( ∧i p _) = p
∧e₂ :
{ l m : Level }
{ P : Prop l }
{ Q : Prop m }
→
P ∧ Q → Q
∧e₂ ( ∧i _ q ) = q
infix 3 _↔_
_↔_ : { l : Level } → Prop l → Prop l → Prop l
P ↔ Q = ( P → Q ) ∧ ( Q → P )
data Inhabited { l : Level }( A : Set l ) : Prop l where
inhab : ( x : A ) → Inhabited A
infix 1 ∃
data ∃ { l m : Level }( A : Set l )( P : A → Prop m ) : Prop ( l ⊔ m ) where
∃i : ( x : A )( p : P x ) → ∃ A P
syntax ∃ A (λ x → P ) = ∃ x ∶ A , P
infix 1 ∃!
∃! : { l m : Level }( A : Set l )( P : A → Prop m ) → Prop ( l ⊔ m )
∃! A P = ∃ x ∶ A , ( P x ∧ ∀( x' : A ) → P x' → x == x' )
syntax ∃! A (λ x → P ) = ∃! x ∶ A , P
infix 1 ⋀
data ⋀ { l m : Level }( P : Prop l )( Q : P → Prop m ) : Prop ( l ⊔ m ) where
⋀i : ( x : P )( p : Q x ) → ⋀ P Q
syntax ⋀ P (λ p → Q ) = ⋀ p ∶ P , Q
⋀e₁ :
{ l m : Level }
{ P : Prop l }
{ Q : P → Prop m }
→
⋀ P Q → P
⋀e₁ ( ⋀i p _) = p
⋀e₂ :
{ l m : Level }
{ P : Prop l }
{ Q : P → Prop m }
( ⋀pq : ⋀ P Q )
→
Q ( ⋀e₁ ⋀pq )
⋀e₂ ( ⋀i _ q ) = q
infixr 1 _∨_
data _∨_ { l m : Level }( P : Prop l )( Q : Prop m ) : Prop ( l ⊔ m ) where
∨i₁ : P → P ∨ Q
∨i₂ : Q → P ∨ Q
case :
{ l m : Level }
{ A : Set l }
{ B : A → Set m }
( x : A )
( f : ( x : A ) → B x )
→
B x
case x f = f x
casep :
{ l m : Level }
{ A : Set l }
{ P : A → Prop m }
( x : A )
( p : ( x : A ) → P x )
→
P x
casep x p = p x
match :
{ l m : Level }
{ P : Prop l }
{ Q : P → Prop m }
( p : P )
( q : ∀ p → Q p )
→
Q p
match p q = q p
infixl 4 _∣_
record set
{ l m : Level }
( A : Set l )
( P : A → Prop m )
:
Set ( l ⊔ m )
where
constructor _∣_
field
el : A
pf : P el
open set public
syntax set A (λ x → P ) = set x ∶ A , P
setext :
{ l m : Level }
{ A : Set l }
{ P : A → Prop m }
{ z z' : set A P }
( _ : el z == el z' )
→
z == z'
setext { z = _ ∣ _} {_ ∣ _} refl = refl
injection :
{ l m : Level }
{ A : Set l }
{ B : Set m }
( f : A → B )
→
Prop ( l ⊔ m )
injection f = ∀{ x x' } → f x == f x' → x == x'
surjection :
{ l m : Level }
{ A : Set l }
{ B : Set m }
( q : B → A )
→
Prop ( l ⊔ m )
surjection q = ∀ x → ∃ y ∶ _ , q y == x
bijection :
{ l m : Level }
{ A : Set l }
{ B : Set m }
( f : A → B )
→
Prop ( l ⊔ m )
bijection f = injection f ∧ surjection f
∏ :
{ l m : Level }
( A : Set l )
( B : A → Set m )
→
Set ( l ⊔ m )
∏ A B = ( x : A ) → B x
syntax ∏ A (λ x → B ) = ∏ x ∶ A , B
infixr 4 _,_
record ∑ { l m : Level }( A : Set l )( B : A → Set m ) : Set ( l ⊔ m ) where
constructor _,_
field
fst : A
snd : B fst
{-# BUILTIN SIGMA ∑ #-}
open ∑ public
infix 2 ∑-syntax
∑-syntax : { l m : Level }( A : Set l ) → ( A → Set m ) → Set ( l ⊔ m )
∑-syntax = ∑
syntax ∑-syntax A (λ x → B ) = ∑ x ∶ A , B
pair :
{ l m : Level }
{ A : Set l }
( B : A → Set m )
( x : A )
( _ : B x )
→
∑ A B
pair _ x y = ( x , y )
∑ext :
{ l m : Level }
{ A : Set l }
{ B : A → Set m }
{ x x' : A }
{ y : B x }
{ y' : B x' }
( _ : x == x' )
( _ : y === y' )
→
pair B x y == pair B x' y'
∑ext refl refl = refl
∑heq₁ :
{ l m : Level }
{ A A' : Set l }
{ B : A → Set m }
{ B' : A' → Set m }
{ x : A }
{ x' : A' }
{ y : B x }
{ y' : B' x' }
( _ : A == A' )
( _ : B === B' )
( _ : pair B x y === pair B' x' y' )
→
x === x'
∑heq₁ refl refl refl = refl
∑heq₂ :
{ l m : Level }
{ A A' : Set l }
{ B : A → Set m }
{ B' : A' → Set m }
{ x : A }
{ x' : A' }
{ y : B x }
{ y' : B' x' }
( _ : A == A' )
( _ : B === B' )
( _ : pair B x y === pair B' x' y' )
→
y === y'
∑heq₂ refl refl refl = refl
record ∑ₚ { l m : Level }( P : Prop l )( B : P → Set m ) : Set ( l ⊔ m ) where
constructor _,_
field
fst : P
snd : B fst
open ∑ₚ public
infix 2 ∑ₚ-syntax
∑ₚ-syntax : { l m : Level }( P : Prop l ) → ( P → Set m ) → Set ( l ⊔ m )
∑ₚ-syntax = ∑ₚ
syntax ∑ₚ-syntax P (λ p → B ) = ∑ₚ p ∶ P , B
pairₚ :
{ l m : Level }
{ P : Prop l }
( B : P → Set m )
( x : P )
( _ : B x )
→
∑ₚ P B
pairₚ _ x y = ( x , y )
∑ₚheq :
{ l m : Level }
{ P P' : Prop l }
{ B : P → Set m }
{ B' : P' → Set m }
{ x : P }
{ x' : P' }
{ y : B x }
{ y' : B' x' }
( _ : P == P' )
( _ : B === B' )
( _ : pairₚ B x y === pairₚ B' x' y' )
→
y === y'
∑ₚheq refl refl refl = refl
uncurry :
{ l m n : Level }
{ A : Set l }
{ B : A → Set m }
{ C : ( a : A ) → B a → Set n }
( f : ( a : A ) ( b : B a ) → C a b )
→
( x : ∑ A B ) → C ( fst x ) ( snd x )
uncurry f ( fst , snd ) = f fst snd
infixr 5 _×_
_×_ : { l m : Level } → Set l → Set m → Set ( l ⊔ m )
A × B = ∑ A (λ _ → B )
record 𝟙 : Set where
instance constructor tt
{-# BUILTIN UNIT 𝟙 #-}
record Unit { l : Level } : Set l where
instance constructor unit
infixr 1 _+_
data _+_ { l m : Level }( A : Set l )( B : Set m ) : Set ( l ⊔ m ) where
ι₁ : ( x : A ) → A + B
ι₂ : ( y : B ) → A + B
_+'_ :
{ l m n : Level }
{ X : Set l }
( A : X → Set m )
( B : X → Set n )
( x : X )
→
Set ( m ⊔ n )
( A +' B ) x = A x + B x
[_,_] :
{ l m n : Level }
{ A : Set l }
{ B : Set m }
{ C : A + B → Set n } →
( f : ( x : A ) → C ( ι₁ x ))
( g : ( x : B ) → C ( ι₂ x ))
→
( x : A + B ) → C x
[ f , g ] ( ι₁ x ) = f x
[ f , g ] ( ι₂ y ) = g y
data ℕ : Set where
zero : ℕ
suc : ( n : ℕ ) → ℕ
{-# BUILTIN NATURAL ℕ #-}
pattern _+1 n = suc n
infix 4 _≐_
_≐_ : ℕ → ℕ → 𝔹
zero ≐ zero = true
zero ≐ ( n +1 ) = false
( m +1 ) ≐ zero = false
( m +1 ) ≐ ( n +1 ) = m ≐ n
decidableℕ : ( m n : ℕ ) → m == n ∨ ¬ ( m == n )
decidableℕ zero zero = ∨i₁ refl
decidableℕ zero ( n +1 ) = ∨i₂ λ{()}
decidableℕ ( m +1 ) zero = ∨i₂ λ{()}
decidableℕ ( m +1 ) ( n +1 ) with decidableℕ m n
... | ∨i₁ refl = ∨i₁ refl
... | ∨i₂ p = ∨i₂ λ{ refl → p refl }
infixr 6 _∷_
data List { l : Level }( A : Set l ) : Set l where
[] : List A
_∷_ : ( x : A )( xs : List A ) → List A
{-# BUILTIN LIST List #-}
module _
{ l m : Level }
{ A : Set l }
{ B : A → Set m }
( f : ( x : A ) → B x )
where
ker : Set ( l ⊔ m )
ker = set ( x , x' ) ∶ A × A , ( f x === f x' )
πker₁ : ker → A
πker₁ (( x , _) ∣ _) = x
πker₂ : ker → A
πker₂ ((_ , x' ) ∣ _) = x'
eqker : ( z : ker ) → f ( πker₁ z ) === f ( πker₂ z )
eqker ((_ , _) ∣ e ) = e