```{-# OPTIONS --without-K #-}
module function.isomorphism.two-out-of-six where

open import sum
open import equality
open import function.core
open import function.isomorphism.core
open import hott.equivalence.core
open import hott.equivalence.biinvertible

module two-out-of-six
{i j k l}{X : Set i}{Y : Set j}{Z : Set k}{W : Set l}
(f : X → Y)(g : Y → Z)(h : Z → W)
(gf-equiv : weak-equiv (g ∘ f))
(hg-equiv : weak-equiv (h ∘ g)) where
private
r : X ≅ Z
r = ≈⇒≅ (g ∘ f , gf-equiv)

s : Y ≅ W
s = ≈⇒≅ (h ∘ g , hg-equiv)

gl : Z → Y
gl = invert s ∘ h

gr : Z → Y
gr = f ∘ invert r

g-iso : Y ≅ Z
g-iso = b⇒≅ (g , (gl , _≅_.iso₁ s) , (gr , _≅_.iso₂ r))

f-iso : X ≅ Y
f-iso = record
{ to = f
; from = λ y → invert r (g y)
; iso₁ = _≅_.iso₁ r
; iso₂ = λ y → sym (_≅_.iso₁ g-iso (f (invert r (g y))))
· ap (invert g-iso) (_≅_.iso₂ r (g y))
· _≅_.iso₁ g-iso y }

h-iso : Z ≅ W
h-iso = record
{ to = h
; from = λ w → g (invert s w)
; iso₁ = λ z → sym (ap (λ z → g (invert s (h z))) (_≅_.iso₂ g-iso z))
· ap g (_≅_.iso₁ s (invert g-iso z))
· _≅_.iso₂ g-iso z
; iso₂ = _≅_.iso₂ s }
```