# How to prove \`view\` distributiveness over a lens composition

**URL:** <https://discourse.haskell.org/t/how-to-prove-view-distributiveness-over-a-lens-composition/6826>\
**Category:** Learn\
**Created:** [July 4, 2023, 11:51am UTC](https://discourse.haskell.org/t/how-to-prove-view-distributiveness-over-a-lens-composition/6826 "2023-07-04T11:51:50Z")\
**Posts on this page:** 1\
**Showing post:** 5

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [July 4, 2023, 12:47pm UTC](https://discourse.haskell.org/t/how-to-prove-view-distributiveness-over-a-lens-composition/6826/5 "2023-07-04T12:47:04Z")

</div>

I believe it should be possible to prove something like

```haskell
g . f Const = f (g . Const)
 where
  f :: Lens' A B
  g :: forall x. Const B x -> Const B x

```

---

_[View the full topic](https://discourse.haskell.org/t/how-to-prove-view-distributiveness-over-a-lens-composition/6826)._