← 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/univ/proofs.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/univ/proofs.agda
1
 
 
2
 
module proofs where
3
 
 
4
 
open import univ
5
 
open import cwf
6
 
open import Base
7
 
open import Nat
8
 
open import help
9
 
 
10
 
{-
11
 
lem-id∘ : {Γ Δ : Con}(σ : Γ ─→ Δ) -> id ∘ σ == σ
12
 
lem-id∘ (el < σ , pσ >) = eq \x -> ref
13
 
 
14
 
lem-∘id : {Γ Δ : Con}(σ : Γ ─→ Δ) -> σ ∘ id == σ
15
 
lem-∘id (el < σ , pσ >) = eq \x -> ref
16
 
 
17
 
lem-∘assoc : {Γ Δ Θ Ξ : Con}(σ : Θ ─→ Ξ)(δ : Δ ─→ Θ)(θ : Γ ─→ Δ) ->
18
 
             (σ ∘ δ) ∘ θ == σ ∘ (δ ∘ θ)
19
 
lem-∘assoc (el < σ , pσ >) (el < δ , pδ >) (el < θ , pθ >) = eq \x -> ref
20
 
-}
21
 
 
22
 
lem-/∘ : {Γ Δ Θ : Con}(A : Type Γ)(σ : Δ ─→ Γ)(δ : Θ ─→ Δ) ->
23
 
         A / σ ∘ δ =Ty A / σ / δ
24
 
lem-/∘ A (el < _ , _ >) (el < _ , _ >) = eqTy \x -> refS
25
 
 
26
 
{-
27
 
lem-//id : {Γ : Con}{A : Type Γ}{u : Elem Γ A} -> u // id =El castElem lem-/id u
28
 
lem-//id {Γ}{A}{elem (el < u , pu >)} = eqEl (eq prf)
29
 
  where
30
 
    prf : (x : El Γ) -> _
31
 
    prf x =
32
 
      chain> u x
33
 
         === _ << u (refS << x) by pu (sym (ref<< x))
34
 
         === _ << u (refS << x) by pfi _ _ _
35
 
      where open module C11 = Chain _==_ (ref {_}) (trans {_})
36
 
 
37
 
lem-//∘ : {Γ Δ Θ : Con}{A : Type Γ}(u : Elem Γ A)(σ : Δ ─→ Γ)(δ : Θ ─→ Δ) ->
38
 
          u // σ ∘ δ =El castElem (lem-/∘ A σ δ) (u // σ // δ)
39
 
lem-//∘ {Γ}{Δ}{Θ} (elem (el < u , pu >)) σ'@(el < σ , _ >) δ'@(el < δ , _ >) = eqEl (eq prf)
40
 
  where
41
 
    prf : (x : El Θ) -> _
42
 
    prf x =
43
 
      chain> u (σ (δ x))
44
 
         === _ << u (σ (δ (refS << x))) by pu (p─→ σ' (p─→ δ' (sym (ref<< x))))
45
 
         === _ << u (σ (δ (refS << x))) by pfi _ _ _
46
 
      where open module C12 = Chain _==_ (ref {_}) (trans {_})
47
 
 
48
 
lem-wk∘σ,,u : {Γ Δ : Con}{A : Type Γ}(σ : Δ ─→ Γ)(u : Elem Δ (A / σ)) ->
49
 
              wk ∘ (σ ,, u) == σ
50
 
lem-wk∘σ,,u (el < σ , pσ >) (elem (el < u , pu >)) = eq \x -> ref
51
 
 
52
 
lem-/wk∘σ,,u : {Γ Δ : Con}(A : Type Γ)(σ : Δ ─→ Γ)(u : Elem Δ (A / σ)) ->
53
 
               A / wk / (σ ,, u) =Ty A / σ
54
 
lem-/wk∘σ,,u A (el < σ , pσ >) (elem (el < u , pu >)) = eqTy \x -> refS
55
 
 
56
 
lem-vz/σ,,u : {Γ Δ : Con}{A : Type Γ}(σ : Δ ─→ Γ)(u : Elem Δ (A / σ)) ->
57
 
              vz // (σ ,, u) =El castElem (lem-/wk∘σ,,u A σ u) u
58
 
lem-vz/σ,,u (el < σ , pσ >) (elem (el < u , pu >)) = eqEl (eq \x -> prf x)
59
 
  where
60
 
    prf : (x : El _) -> u x == _ << u (refS << x)
61
 
    prf x =
62
 
      chain> u x
63
 
         === _ << u (refS << x) by pu (sym (ref<< x))
64
 
         === _ << u (refS << x) by pfi _ _ _
65
 
      where open module C15 = Chain _==_ (ref {_}) (trans {_})
66
 
 
67
 
lem-σ,,u∘ : {Γ Δ Θ : Con}{A : Type Γ}
68
 
            (σ : Δ ─→ Γ)(u : Elem Δ (A / σ))(δ : Θ ─→ Δ) ->
69
 
            (σ ,, u) ∘ δ == (σ ∘ δ ,, castElem (lem-/∘ A σ δ) (u // δ))
70
 
lem-σ,,u∘ (el < σ , _ >) (elem (el < u , pu >)) δ'@(el < δ , _ >) =
71
 
  eq \x -> eq < ref , prf x >
72
 
  where
73
 
    prf : (x : El _) -> u (δ x) == _ << _ << u (δ (refS << x))
74
 
    prf x =
75
 
      chain> u (δ x)
76
 
         === _ << u (δ (refS << x)) by pu (p─→ δ' (sym (ref<< x)))
77
 
         === _ << _ << u (δ (refS << x)) by sym (casttrans _ _ _ _)
78
 
      where open module C15 = Chain _==_ (ref {_}) (trans {_})
79
 
 
80
 
lem-wk,,vz : {Γ : Con}{A : Type Γ} -> (wk ,, vz) == id {Γ , A}
81
 
lem-wk,,vz {Γ}{A} = eq prf
82
 
  where
83
 
    prf : (x : El (Γ , A)) -> _
84
 
    prf (el < x , y >) = ref
85
 
-}
86
 
 
87
 
lem-Π/ : {Γ Δ : Con}{A : Type Γ}(B : Type (Γ , A))(σ : Δ ─→ Γ) ->
88
 
         Π A B / σ =Ty Π (A / σ) (B / (σ ∘ wk ,, castElem (lem-/∘ A σ wk) vz))
89
 
lem-Π/ B (el < σ , pσ >) =
90
 
  eqTy \x -> eqS < refS , (\y -> pFam B (eq < ref , prf x y >)) >
91
 
  where
92
 
    postulate prf : (x : El _)(y : El _) -> y == _ << _ << _ << _ << y
93
 
 
94
 
{-
95
 
lem-β : {Γ : Con}{A : Type Γ}{B : Type (Γ , A)}
96
 
        (v : Elem (Γ , A) B)(u : Elem Γ A) ->
97
 
        (ƛ v) ∙ u =El v // [ u ]
98
 
lem-β {Γ}{A}{B} (elem (el < v , pv >)) (elem (el < u , pu >)) = eqEl (eq \x -> prf x _ _)
99
 
  where
100
 
    prf : (x : El Γ)(q : _ =S _)(p : _ =S _) ->
101
 
          p << v (el < x , u x >) == v (el < x , q << u (refS << x) >)
102
 
    prf x q p =
103
 
      chain> p << v (el < x , u x >)
104
 
         === p << q0 << v (el < x , q1 << u (refS << x) >)
105
 
          by p<< p (pv (eqSnd (pu (sym (ref<< x)))))
106
 
         === q2 << v (el < x , q1 << u (refS << x) >)
107
 
          by sym (trans<< p q0 _)
108
 
         === q2 << q3 << v (el < x , q << u (refS << x) >)
109
 
          by p<< q2 (pv (eqSnd (pfi q1 q _)))
110
 
         === v (el < x , q << u (refS << x) >)
111
 
          by castref2 q2 q3 _
112
 
      where
113
 
        open module C17 = Chain _==_ (ref {_}) (trans {_})
114
 
        q0 = _
115
 
        q1 = _
116
 
        q2 = _
117
 
        q3 = _
118
 
 
119
 
-}