And is symmetric

andsym.ctt

module andsym where

Path (A : U) (a b : A) : U = PathP (<_> A) a b

data bool = true | false

and (x:bool) : bool -> bool = split
  true -> x
  false -> false

andtrue : (x:bool) -> Path bool (and true x) x = split
  true -> <i> true
  false -> <i> false

andfalse : (x:bool) -> Path bool (and false x) false = split
  true -> <i> false
  false -> <i> false

andsym (a:bool) : (b:bool) -> Path bool (and a b) (and b a) = split
  true -> <i> andtrue a @ -i
  false -> <i> andfalse a @ -i

Держи рабочее док-во:

andsym: (a b: bool) -> Path bool (and a b) (and b a) = split
  true -> split@((b:bool) -> Path bool (and true b) (and b true)) with
    true -> <i> true
    false -> <i> false
  false -> split@((b:bool) -> Path bool (and false b) (and b false)) with
    true -> <i> false
    false -> <i> false

Cимметричный вариант док-ва

andtruesym : (x:bool) -> Path bool (and true x) (and x true) = split
  true -> <i> true
  false -> <i> false

andfalsesym : (x:bool) -> Path bool (and false x) (and x false) = split
  true -> <i> false
  false -> <i> false

andsym: (a b: bool) -> Path bool (and a b) (and b a) = split
  true -> andtruesym
  false -> andfalsesym