// Homogeneous groupoid operations

theorem Refl(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [a : ty]
   (path [_] ty a a))
by {
  lam ty a => abs _ => `a
}.

theorem Symm(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [p : (line [_] ty)]
   (path [_] ty (@ p 1) (@ p 0)))
by {
  lam ty p => abs x =>
  `(hcom 0~>1 ty (@ p 0)
    [x=0 [y] (@ p y)]
    [x=1 [_] (@ p 0)])
}.

theorem Trans(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [p : (line [_] ty)]
   [q : (line [_] ty)]
   [eq : (= ty (@ p 1) (@ q 0))]
   (path [_] ty (@ p 0) (@ q 1)))
by {
  lam ty p q eq => (abs x =>
    `(hcom 0~>1 ty (@ p x)
      [x=0 [_] (@ p 0)]
      [x=1 [z] (@ q z)]));
    auto; assumption
}.

theorem Symm/Unit(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [a : ty]
   (path [_]
     (path [_] ty a a)
     (abs [_] a)
     ($ (Symm #l) ty (abs [_] a))))
by {
  lam ty a =>
  abs y x =>
  `(hcom 0~>y ty a [x=0 [_] a] [x=1 [_] a])
}.

theorem Trans/Unit/R(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [p : (line [_] ty)]
   (path [_]
     (path [_] ty (@ p 0) (@ p 1))
     p
     ($ (Trans #l) ty p (abs [_] (@ p 1)) ax)))
by {
  lam ty p =>
  (abs y x =>
    `(hcom 0~>y ty (@ p x) [x=0 [_] (@ p 0)] [x=1 [_] (@ p 1)]));

  refine path/eq/from-line; auto
}.

// Thanks to Bruno Bentzen for already doing this and drawing a picture! -Carlo
theorem Trans/Sym/R(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [p : (line [_] ty)]
   (path [_]
     (path [_] ty (@ p 0) (@ p 0))
     (abs [_] (@ p 0))
     ($ (Trans #l) ty p ($ (Symm #l) ty p) ax)))
by {
  lam ty p =>
  (abs z x =>
    `(hcom 0~>1 ty (@ p x)
      [x=0 [_] (@ p 0)]
      [x=1 [y] (@ ($ (Symm #l) ty p) y)]
      [z=0 [y] (hcom 0~>x ty (@ p 0) [y=0 [x] (@ p x)] [y=1 [_] (@ p 0)])]
      [z=1 [y]
        (hcom 0~>y ty (@ p x)
          [x=0 [_] (@ p 0)]
          [x=1 [y] (@ ($ (Symm #l) ty p) y)])]));
  unfold Symm; auto
}.

//// My tests - Bruno

// My first theorem in RedPRL! :D - Bruno

theorem Refl/Inv(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [a : ty]
   (path [_]
     (path [_] ty a a)
     (abs [_] a)
     ($ (Symm #l) ty ($ (Symm #l) ty (abs [_] a) ))  ))
by {
  lam ty a =>
  (abs z x =>
    `(hcom 0~>1 ty a
       [x=0 [y] (@ ($ (Symm/Unit #l) ty a) z y)]
       [x=1 [_] a]
       [z=0 [y] a]
       [z=1 [y] (hcom 0~>y ty (@ ($ (Symm #l) ty (abs [_] a)) 0)
                  [x=0 [y] (@ ($ (Symm #l) ty (abs [_] a)) y)]
                  [x=1 [_] (@ ($ (Symm #l) ty (abs [_] a)) 0)]) ]
     )
  );
  unfold Symm; auto
}.

// Thanks to Carlo for helping me with this! - Bruno

theorem Square/Swap(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [p : (-> dim dim ty)]
   (path [z] (path [_] ty
                   (@ ($ (Symm #l) ty (abs [z] (@ p z 0))) z)
                   (@ ($ (Symm #l) ty (abs [z] (@ p z 1))) z))
         (@ p 1)
         (@ p 0)))
by {
  lam ty p =>
  (abs x z =>
    `(hcom 0~>1 ty (@ p 0 z)
       [x=0 [y] (@ p y z) ]
       [x=1 [_] (@ p 0 z) ]
       [z=0 [y] (hcom 0~>y ty (@ p 0 0)
                  [x=0 [y] (@ p y 0)]
                  [x=1 [_] (@ p 0 0)]) ]
       [z=1 [y] (hcom 0~>y ty (@ p 0 1)
                  [x=0 [y] (@ p y 1)]
                  [x=1 [_] (@ p 0 1)]) ]
     )
  ); auto; symmetry; unfold Symm; refine path/eq/eta;
  [id, refine path/eq/from-line, id, refine path/eq/from-line]; auto
}.

// This is the error message I am getting with this double square swap function:
//      Error resolving abt: SortError
// I suspect that the root of problem here is that ($ (Square/Swap #l) ty (@ p z x))
// is an element of (path [z] (path [_] ty ...) while Square/Swap is expecting an
// object of (-> dim dim ty).
// If this is the case, can we cast the former type into the latter?

theorem Double/Swap(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [p : (-> dim dim ty)]
   (path [z] (path [_] ty
                   (@ ($ (Symm #l) ty ($ (Symm #l) ty (abs [z] (@ p z 0)))) z)
                   (@ ($ (Symm #l) ty ($ (Symm #l) ty (abs [z] (@ p z 1)))) z))
         (@ p 0)
         (@ p 1)))
by {
  lam ty p =>
  (abs z x =>
    ($ (Square/Swap #l) ty ($ (Square/Swap #l) ty (@ p z x)))
  );
  auto
}.

// The reason I need double square swap is to mechanize my proof that p = p^-1^-1:

//theorem Sym/Inv(#l:lvl) :
//  (->
//   [ty : (U #l kan)]
//   [p : (line [_] ty)]
//   (path [_] (path [_] ty
//                   (@ p 0)
//                   (@ p 1))
//     p
//     ($ (Symm #l) ty ($ (Symm #l) ty p ))  ))
//by {
//  lam ty a =>
//  (abs z x =>
//    `(hcom 0~>1 ty (@ ($ (Refl/Inv #l) ty (@ p 0) ) z x)
//       [x=0 [y] (@ ($ (Symm #l) ty p) y)]
//       [x=1 [_] ($ (Trans #l) ty ($ (Symm #l) ty p) p ax) ]
//       [z=0 [y] (hcom 0~>x ty  (@ ($ (Symm #l) ty p) y)
//                  [y=0 [_] (@ p 1)]
//                  [y=1 [x] (@ p x)]) ]
//
//       [z=1 [y] ...Needs the Double/Swap of the above hcom here... ]
//     )
//  );
//  unfold Symm; auto
//}.

// This is another proof I am stuck with:
//    22 Remaining obligations
// Am I doing something silly here again?

theorem Square/Op(#l:lvl) :
  (->
   [ty : (U #l kan)]
   [p : (line [_] ty)]
   (path [z] (path [_] ty
                   (@ p 0)
                   (@ ($ (Symm #l) ty p) z) )
     p
     (abs [_] (@ p 0)) ))
by {
  lam ty p =>
  (abs z x =>
    `(hcom 0~>1 ty (hcom 0~>z ty (@ p x)
                     [x=0 [_] (@ p 0)]
		     [x=1 [z] (@ ($ (Symm #l) ty p) z)])
      [x=0 [_] (@ p 0)]
      [x=1 [_] (@ ($ (Symm #l) ty p) z)]
      [z=0 [_] (@ p x)]
      [z=1 [y] (@ ($ (Symm #l) ty
                          ($ (Trans/Sym/R #l) ty p)
                  )
                y x) ]
   ));
  unfold Symm; auto
}.

//// End - Bruno

// Heterogeneous groupoid operations

theorem DSymm(#l:lvl) :
  (->
   [ty : (line [_] (U #l kan))]
   [p : (line [x] (@ ty x))]
   (path [x]
     (@ ($ (Symm (++ #l)) (U #l kan) ty) x)
     (@ p 1)
     (@ p 0)))
by {
  lam ty p =>
  (abs x =>
  `(com 0~>1
    [y] (hcom 0~>y (U #l kan) (@ ty 0) [x=0 [y] (@ ty y)] [x=1 [_] (@ ty 0)])
    (@ p 0)
    [x=0 [y] (@ p y)]
    [x=1 [_] (@ p 0)]));
  unfold Symm; auto
}.