← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/iird/Identity.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/iird/Identity.agda
1
 
 
2
 
module Identity where
3
 
 
4
 
data _==_ {A : Set}(x : A) : A -> Set where
5
 
  refl : x == x
6
 
 
7
 
elim== : {A : Set}(x : A)(C : (y : A) -> x == y -> Set) ->
8
 
         C x refl -> (y : A) -> (p : x == y) -> C y p
9
 
elim== x C Cx .x refl = Cx
10
 
 
11
 
elim==₁ : {A : Set}(x : A)(C : (y : A) -> x == y -> Set1) ->
12
 
          C x refl -> (y : A) -> (p : x == y) -> C y p
13
 
elim==₁ x C Cx .x refl = Cx
14
 
 
15
 
sym : {A : Set}{x y : A} -> x == y -> y == x
16
 
sym {A}{x}{y} eq = elim== x (\z _ -> z == x) refl y eq
17
 
 
18
 
cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
19
 
cong {A} f {x}{y} eq = elim== x (\z _ -> f x == f z) refl y eq
20
 
 
21
 
subst : {A : Set}{x y : A}(P : A -> Set) -> x == y -> P x -> P y
22
 
subst P xy px = elim== _ (\z _ -> P z) px _ xy
23
 
 
24
 
subst₁ : {A : Set}{x y : A}(P : A -> Set1) -> x == y -> P x -> P y
25
 
subst₁ P xy px = elim==₁ _ (\z _ -> P z) px _ xy
26
 
 
27
 
symRef : (A : Set)(x : A) -> sym (refl{A}{x}) == refl
28
 
symRef A x = refl
29
 
 
30
 
symSym : {A : Set}{x y : A}(p : x == y) -> sym (sym p) == p
31
 
symSym {A}{x}{y} p = elim== x (\y q -> sym (sym q) == q) refl y p
32
 
 
33
 
elimS : {A : Set}(x : A)(C : (y : A) -> y == x -> Set) ->
34
 
        C x refl -> (y : A) -> (p : y == x) -> C y p
35
 
elimS x C r y p = subst (C y) (symSym p) h
36
 
  where
37
 
    h : C y (sym (sym p))
38
 
    h = elim== x (\y p -> C y (sym p)) r y (sym p)
39
 
 
40
 
data _==¹_ {A : Set1}(x : A) : {B : Set1} -> B -> Set where
41
 
  refl¹ : x ==¹ x
42
 
 
43
 
subst¹ : {A : Set1}{x y : A}(P : A -> Set) -> x ==¹ y -> P x -> P y
44
 
subst¹ {A} P refl¹ px = px
45