Last active
March 12, 2026 22:46
-
-
Save clayrat/5ff21b21ac74bbaece421c3e8fd1de21 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --safe #-} | |
| open import Cat.Prelude | |
| import Cat.Morphism | |
| import Cat.Diagram.Pullback | |
| module PullbackLemma {ℓ ℓ′} (Cat : Precategory ℓ ℓ′) where | |
| open Cat.Morphism Cat | |
| open Cat.Diagram.Pullback Cat | |
| pullback-lemma-bwd : ∀ {A B C D E F : Ob} | |
| (f : A ⇒ B) (g : B ⇒ C) | |
| (h : D ⇒ E) (i : E ⇒ F) | |
| (u : A ⇒ D) (v : B ⇒ E) (w : C ⇒ F) | |
| → is-pullback g w v i | |
| → is-pullback (g ∘ f) w u (i ∘ h) | |
| → v ∘ f ＝ h ∘ u | |
| → is-pullback f v u h | |
| pullback-lemma-bwd f g h i u v w pr pb eq .is-pullback.square = eq | |
| pullback-lemma-bwd f g h i u v w pr pb eq .is-pullback.has-pb-for {P′} {p₁′} {p₂′} = | |
| record { | |
| universal = λ e → pb′ .is-pullback-for.universal $ eq′ e | |
| ; p₁∘universal = λ {p} → | |
| let ub = pb′ .is-pullback-for.universal (eq′ p) in | |
| pr′ .is-pullback-for.unique {p = eq′ p ∙ assoc p₂′ h i} {lim′ = f ∘ ub} | |
| ( assoc ub f g ⁻¹ | |
| ∙ pb′ .is-pullback-for.p₁∘universal {p = eq′ p}) | |
| ( assoc ub f v ⁻¹ | |
| ∙ ap (_∘ ub) eq | |
| ∙ assoc ub u h | |
| ∙ ap (h ∘_) | |
| (pb′ .is-pullback-for.p₂∘universal {p = eq′ p})) | |
| ∙ pr′ .is-pullback-for.unique {p = eq′ p ∙ assoc p₂′ h i} {lim′ = p₁′} refl p ⁻¹ | |
| ; p₂∘universal = λ {p} → pb′ .is-pullback-for.p₂∘universal {p = eq′ p} | |
| ; unique = λ {p} {lim′} e1 e2 → | |
| pb′ .is-pullback-for.unique {p = eq′ p} | |
| (assoc lim′ f g ∙ ap (g ∘_) e1) e2 | |
| } | |
| where | |
| pb′ = pb .is-pullback.has-pb-for {P′} {p₁′ = g ∘ p₁′} {p₂′ = p₂′} | |
| pr′ = pr .is-pullback.has-pb-for {P′} {p₁′ = g ∘ p₁′} {p₂′ = h ∘ p₂′} | |
| eq′ : v ∘ p₁′ ＝ h ∘ p₂′ → w ∘ g ∘ p₁′ ＝ (i ∘ h) ∘ p₂′ | |
| eq′ p = assoc p₁′ g w ⁻¹ | |
| ∙ ap (_∘ p₁′) (pr .is-pullback.square) | |
| ∙ assoc p₁′ v i | |
| ∙ ap (i ∘_) p | |
| ∙ assoc p₂′ h i ⁻¹ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment