Data.Telescope.Congruence

N-ary congruence for reasoning

Definitions

congType : (delta : Segment n gamma) -> (env1 : Environment gamma) -> (sy1 : SimpleFun env1 delta Type) -> Fun env1 delta sy1 -> (env2 : Environment gamma) -> (sy2 : SimpleFun env2 delta Type) -> Fun env2 delta sy2 -> Type

Visibility: public export

congSegment : (0 delta : Segment n gamma) -> (0 env1 : Environment gamma) -> (0 sy1 : SimpleFun env1 delta Type) -> (0 lhs : Fun env1 delta sy1) -> (0 env2 : Environment gamma) -> (0 sy2 : SimpleFun env2 delta Type) -> (0 rhs : Fun env2 delta sy2) -> (0 _ : env1 = env2) -> (0 _ : sy1 = sy2) -> (0 _ : lhs = rhs) -> congType delta env1 sy1 lhs env2 sy2 rhs

Visibility: public export

cong : (context : Fun () delta sy) -> congType delta () sy context () sy context

Visibility: public export