Proposition frobenius_reciprocity {H : first_order_hyperdoctrine} {Γ A : ty H} (φ : form (Γ ×h A)) (Δ : form Γ) : Δ ∧ (∃h φ) ⊢ (∃h (Δ [ π₁ (tm_var (Γ ×h A)) ] ∧ φ)). Proof. enough (∃h φ ⊢ Δ ⇒ ∃h (Δ [ π₁ (tm_var (Γ ×h A)) ] ∧ φ)) as r₁. { assert (Δ ∧ ∃h φ ⊢ Δ ⇒ ∃h (Δ [ π₁ (tm_var (Γ ×h A)) ] ∧ φ)) as r₂. { use weaken_right. exact r₁. } refine (impl_elim _ r₂). use weaken_left. apply hyperdoctrine_hyp. } use (exists_elim_empty (hyperdoctrine_hyp _)). rewrite impl_subst. use impl_intro. rewrite exists_subst. use exists_intro. - exact (π₂ (tm_var _)). - rewrite hyperdoctrine_comp_subst. rewrite hyperdoctrine_pair_subst. rewrite tm_subst_comp. rewrite hyperdoctrine_pair_comp_pr1. rewrite hyperdoctrine_pair_comp_pr2. rewrite tm_subst_var. rewrite conj_subst. rewrite hyperdoctrine_comp_subst. rewrite hyperdoctrine_pair_comp_pr1. rewrite <- hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. use hyp_sym. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation.