我们考虑构建由类别 p : D → C 的函子生成的自由双纤维化的问题。 这个问题以前由Lamarche考虑,并且与Dawson,Paré和Pronk认为“自由相邻相邻”的问题密切相关。 我们开发一种解决问题的证明理论方法,从自由双纤维化 Λ_p 的构建开始:Bif(p)→C,其中Bif(p)的对象是原始“bifibrational logic”的公式,箭头是无切序列微积分模量概念的推导。 我们表明,将构造实例化到身份functor会产生一个_zigzag double category_Z(C),这也是C上与同伴和连体(或纤维素双类)的免费双类。 该方法可以顺利地适应构建(P,N)-颤动的更一般的任务,其中人们只要求沿着P中的箭头推进,并且在某些箭头中沿着箭头的回调,其中包括Kock和Joyal在(P,N)形成因子化系统时_ambifibration_的概念。 我们建立了一系列逐渐更强的正常形式,以证明理论的 _focusing_ 思想为指导,并在假设基础类别是相对于 P 和 N 的因子化预序下获得规范的结果。 这种规范结果使我们能够决定单词问题,并列举没有重复的相对集合。 最后,我们描述了几个组合性质的例子,包括作为自由除颤在ω上产生的平面树类别,以及作为Δ的自由模棱两可产生的增加的森林类别,其中包含非交叉分区的格子,作为Beck-Chevalley条件的纤维的引物。