Idris2Doc : Data.Telescope.Congruence

Data.Telescope.Congruence

cong : (context : FunMkUnitdeltasy) -> congTypedeltaMkUnitsycontextMkUnitsycontext
congSegment : (0 delta : Segmentngamma) -> (0 env1 : Environmentgamma) -> (0 sy1 : SimpleFunenv1delta Type) -> (0 lhs : Funenv1deltasy1) -> (0 env2 : Environmentgamma) -> (0 sy2 : SimpleFunenv2delta Type) -> (0 rhs : Funenv2deltasy2) -> (0 _ : env1 = env2) -> (0 _ : sy1 = sy2) -> (0 _ : lhs = rhs) -> congTypedeltaenv1sy1lhsenv2sy2rhs
congType : (delta : Segmentngamma) -> (env1 : Environmentgamma) -> (sy1 : SimpleFunenv1delta Type) -> Funenv1deltasy1 -> (env2 : Environmentgamma) -> (sy2 : SimpleFunenv2delta Type) -> Funenv2deltasy2 -> Type