← 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/clowns/ChainRule.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/clowns/ChainRule.agda
1
 
 
2
 
module ChainRule where
3
 
 
4
 
  import Sets
5
 
  import Functor
6
 
  import Logic.ChainReasoning.Poly as CR
7
 
  import Isomorphism
8
 
  import Derivative
9
 
 
10
 
  open Derivative
11
 
  open Sets
12
 
  open Functor
13
 
  open Semantics
14
 
  open Isomorphism
15
 
  module Chain = CR _==_ (\x -> refl{x = x}) (\x y z -> trans{x = x}{y}{z})
16
 
  open Chain
17
 
 
18
 
  chain-rule : (F G : U)(X : Set) -> ⟦ ∂ (F [ G ]) ⟧ X ≅ ⟦ ∂ F [ G ] × ∂ G ⟧ X
19
 
  chain-rule F G X = iso (i F) (j F) (ji F) (ij F)
20
 
    where
21
 
      i : (F : U) -> ⟦ ∂ (F [ G ]) ⟧ X -> ⟦ ∂ F [ G ] × ∂ G ⟧ X
22
 
      i (K A)     ()
23
 
      i Id        x                 = < <> , x >
24
 
      i (F₁ + F₂) (inl c)           = (inl <×> id) (i F₁ c)
25
 
      i (F₁ + F₂) (inr c)           = (inr <×> id) (i F₂ c)
26
 
      i (F₁ × F₂) (inl < c  , f₂ >) = (inl ∘ <∙, f₂ > <×> id) (i F₁ c)
27
 
      i (F₁ × F₂) (inr < f₁ , c  >) = (inr ∘ < f₁ ,∙> <×> id) (i F₂ c)
28
 
 
29
 
      j : (F : U) -> ⟦ ∂ F [ G ] × ∂ G ⟧ X -> ⟦ ∂ (F [ G ]) ⟧ X
30
 
      j (K A)     < () , _ >
31
 
      j Id        < <> , x > = x
32
 
      j (F₁ + F₂) < inl x , y > = inl (j F₁ < x , y >)
33
 
      j (F₁ + F₂) < inr x , y > = inr (j F₂ < x , y >)
34
 
      j (F₁ × F₂) < inl < x , y > , z > = inl < j F₁ < x , z > , y >
35
 
      j (F₁ × F₂) < inr < x , y > , z > = inr < x , j F₂ < y , z > >
36
 
 
37
 
      ij : (F : U)(x : _) -> i F (j F x) == x
38
 
      ij (K A)     < () , _ >
39
 
      ij Id        < <> , x > = refl
40
 
      ij (F₁ + F₂) < lx@(inl x) , y > =
41
 
        subst (\ ∙ -> (inl <×> id) ∙ == < lx , y >)
42
 
              (ij F₁ < x , y >) refl
43
 
      ij (F₁ + F₂) < rx@(inr x) , y > =
44
 
        subst (\ ∙ -> (inr <×> id) ∙ == < rx , y >)
45
 
              (ij F₂ < x , y >) refl
46
 
      ij (F₁ × F₂) < xy@(inl < x , y >) , z > =
47
 
        subst (\ ∙ -> (inl ∘ <∙, y > <×> id) ∙ == < xy , z >)
48
 
              (ij F₁ < x , z >) refl
49
 
      ij (F₁ × F₂) < xy@(inr < x , y >) , z > =
50
 
        subst (\ ∙ -> (inr ∘ < x ,∙> <×> id) ∙ == < xy , z >)
51
 
              (ij F₂ < y , z >) refl
52
 
 
53
 
      ji : (F : U)(y : _) -> j F (i F y) == y
54
 
      ji (K A) ()
55
 
      ji Id x = refl
56
 
      ji (F₁ + F₂) (inl c) =
57
 
        chain> j (F₁ + F₂) ((inl <×> id) (i F₁ c))
58
 
           === inl (j F₁ _)         by cong (j (F₁ + F₂) ∘ (inl <×> id)) (η-[×] (i F₁ c))
59
 
           === inl (j F₁ (i F₁ c))  by cong (inl ∘ j F₁) (sym $ η-[×] (i F₁ c))
60
 
           === inl c                by cong inl (ji F₁ c)
61
 
      ji (F₁ + F₂) rc @ (inr c) =
62
 
        subst (\ ∙ -> j (F₁ + F₂) ((inr <×> id) ∙) == rc) (η-[×] (i F₂ c))
63
 
        $ subst (\ ∙ -> inr (j F₂ ∙) == rc) (sym $ η-[×] (i F₂ c))
64
 
        $ subst (\ ∙ -> inr ∙ == rc) (ji F₂ c) refl
65
 
      ji (F₁ × F₂) l @ (inl < c , f₂ >) =
66
 
        subst (\ ∙ -> j (F₁ × F₂) ((inl ∘ <∙, f₂ > <×> id) ∙) == l) (η-[×] (i F₁ c))
67
 
        $ subst (\ ∙ -> inl < j F₁ ∙ , f₂ > == l) (sym $ η-[×] (i F₁ c))
68
 
        $ subst (\ ∙ -> inl < ∙ , f₂ > == l) (ji F₁ c) refl
69
 
      ji (F₁ × F₂) r @ (inr < f₁ , c >) =
70
 
        subst (\ ∙ -> j (F₁ × F₂) ((inr ∘ < f₁ ,∙> <×> id) ∙) == r) (η-[×] (i F₂ c))
71
 
        $ subst (\ ∙ -> inr < f₁ , j F₂ ∙ > == r) (sym $ η-[×] (i F₂ c))
72
 
        $ subst (\ ∙ -> inr < f₁ , ∙ > == r) (ji F₂ c) refl
73