case h.h
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a = (flip p ∘r flip r) c a
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
⊢ flip (r ∘r p) = flip p ∘r flip r
funext c a
case h.h.a
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a ↔ (flip p ∘r flip r) c a
case h.h
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a = (flip p ∘r flip r) c a
apply propext
case h.h.a.mp
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a → (flip p ∘r flip r) c a

case h.h.a.mpr
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a
case h.h.a
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a ↔ (flip p ∘r flip r) c a
constructor
case h.h.a.mpr
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a
case h.h.a.mp
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a → (flip p ∘r flip r) c a

case h.h.a.mpr
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a
exact fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩
no goals
case h.h.a.mpr
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.12462
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a
exact fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩