Some cube stuff and some stuff on families/fibrations.

1-hits/Alg1/Eq/Cube.agda

@@ -76,3 +76,16 @@ alg₁-hom=-cube' {𝓧} {𝓨} {alg₁-hom (alg₀-hom f f₀) f₁} {alg₁-ho
     𝓰'_ = alg₀-hom g g₀
     𝓯_ = alg₁-hom 𝓯'_ f₁
     𝓰_ = alg₁-hom 𝓰'_ g₁
+
+alg₁-hom=-cube'' :
+  {𝓧 𝓨 : Alg₁-obj}
+  {𝓯 𝓰 : Alg₁-hom 𝓧 𝓨}
+  (p : f 𝓯 == f 𝓰)
+  (p₀ : (x : ⟦ F₀ ⟧₀ (X 𝓧))
+         → Square (f₀ 𝓯 x) (app= p (θ₀ 𝓧 x)) (ap (λ h → (θ₀ 𝓨) (⟦ F₀ ⟧₁ h x)) p) (f₀ 𝓰 x))
+  (p₁ : (x : ⟦ F₁ ⟧₀ (X 𝓧))
+      → ! (f₁ 𝓯 x) ∙h⊡ other-square (𝓧' 𝓧) (𝓧' 𝓨) (θ₁ 𝓧) (θ₁ 𝓨) x (𝓯' 𝓯) (𝓯' 𝓰) p p₀ ==
+        square-apd (λ h → θ₁ 𝓨 (⟦ F₁ ⟧₁ h x)) p ⊡h∙ ! (f₁ 𝓰 x)
+      )
+  → 𝓯 == 𝓰
+alg₁-hom=-cube'' {𝓧} {𝓨} {alg₁-hom (alg₀-hom f f₀) f₁} {alg₁-hom (alg₀-hom g g₀) g₁} p p₀ p₁ = admit _

1-hits/Cube.agda

@@ -50,6 +50,11 @@ module _ {i j}
     → Square (f x) (ap h p) (ap k p) (f y)
   square-apd = ↓-='-to-square ∘ apd f
 
+  square-apd-idp=ids :
+    {x : A}
+    → square-apd {x} {x} idp == horiz-degen-square idp
+  square-apd-idp=ids = idp
+
   square-apd=apd :
     {x y : A}
     (p : x == y)

Dep.agda

@@ -3,6 +3,7 @@
 module Dep where
 
 import dep.Core
+import dep.Fam
 import dep.Fib
-import dep.FibCorrect
+import dep.FamCorrect
 import dep.Sect

README.agda

@@ -30,4 +30,3 @@ import Nondep
 
 -- Restricted specification of 1-HITs, using containers.
 import 1-hits
-

dep/Fam.agda

@@ -0,0 +1,144 @@
+{-# OPTIONS --without-K #-}
+
+module dep.Fam where
+
+open import lib.Basics
+open import Cat
+open import dep.Core
+
+-- Families over a given algebra
+Fam : (s : Spec) → / Alg s / → Type1
+
+□-F :
+  (s : Spec)
+  (F : Alg s ⇒ TypeCat)
+  (𝓧 : / Alg s /)
+  (P : Fam s 𝓧)
+  → F ⋆ 𝓧 → Type0
+
+□-G :
+  (s : Spec)
+  (F : Alg s ⇒ TypeCat)
+  (G : ∫ (Alg s) F ⇒ TypeCat)
+  (𝓧 : / Alg s /)
+  (P : Fam s 𝓧)
+  (x : F ⋆ 𝓧)
+  (y : □-F s F 𝓧 P x)
+  → G ⋆ (𝓧 , x) → Type0
+
+total :
+  (s : Spec)
+  (𝓧 : / Alg s /)
+  → Fam s 𝓧 → / Alg s /
+
+proj :
+  (s : Spec)
+  (𝓧 : / Alg s /)
+  (P : Fam s 𝓧)
+  → Alg s [ total s 𝓧 P , 𝓧 ]
+
+φ-F :
+  (s : Spec)
+  (F : Alg s ⇒ TypeCat)
+  (𝓧 : / Alg s /)
+  (P : Fam s 𝓧)
+  → Σ (F ⋆ 𝓧) (□-F s F 𝓧 P) → F ⋆ (total s 𝓧 P)
+
+φ⁻¹-F :
+  (s : Spec)
+  (F : Alg s ⇒ TypeCat)
+  (𝓧 : / Alg s /)
+  (P : Fam s 𝓧)
+  → F ⋆ (total s 𝓧 P) → Σ (F ⋆ 𝓧) (□-F s F 𝓧 P)
+
+φ-G :
+  (s : Spec)
+  (F : Alg s ⇒ TypeCat)
+  (G : ∫ (Alg s) F ⇒ TypeCat)
+  (𝓧 : / Alg s /)
+  (P : Fam s 𝓧)
+  (x : F ⋆ 𝓧)
+  (y : □-F s F 𝓧 P x)
+  → Σ (G ⋆ (𝓧 , x)) (□-G s F G 𝓧 P x y) → G ⋆ (total s 𝓧 P , φ-F s F 𝓧 P (x , y))
+
+φ⁻¹-G :
+  (s : Spec)
+  (F : Alg s ⇒ TypeCat)
+  (G : ∫ (Alg s) F ⇒ TypeCat)
+  (𝓧 : / Alg s /)
+  (P : Fam s 𝓧)
+  (x : F ⋆ 𝓧)
+  (y : □-F s F 𝓧 P x)
+  → G ⋆ (total s 𝓧 P , φ-F s F 𝓧 P (x , y)) → Σ (G ⋆ (𝓧 , x)) (□-G s F G 𝓧 P x y)
+
+Fam ε X
+  = X → Type0
+Fam (s ▸ mk-constr F G) (𝓧 , θ)
+  = Σ (Fam s 𝓧) (λ P → (x : Σ (F ⋆ 𝓧) (□-F s F 𝓧 P)) → □-G s F G 𝓧 P (fst x) (snd x) (θ (fst x)))
+
+□-F s F 𝓧 P x
+  = Σ (F ⋆ total s 𝓧 P) (λ y → (F ⋆⋆ proj s 𝓧 P) y == x)
+
+φ-F s F 𝓧 P (x , y , p)
+  = y
+
+φ⁻¹-F s F 𝓧 P x
+  = ((F ⋆⋆ proj s 𝓧 P) x) , (x , idp)
+
+□-G s F G 𝓧 P x y p
+  = Σ (G ⋆ (total s 𝓧 P) , φ-F s F 𝓧 P (x , y)) (λ q →
+      (G ⋆⋆ (proj s 𝓧 P) , snd y) q == p)
+
+φ-G s F G 𝓧 P x y (p , q , r)
+  = q
+
+φ⁻¹-G s F G 𝓧 P x y p
+  = ((G ⋆⋆ (proj s 𝓧 P) , (snd y)) p) , (p , idp)
+
+total ε X P
+  = Σ X P
+total (s ▸ mk-constr F G) (𝓧 , θ) (P , m)
+  = (total s 𝓧 P)
+  , (λ x → φ-G s F G 𝓧 P
+               (fst (φ⁻¹-F s F 𝓧 P x))
+               (snd (φ⁻¹-F s F 𝓧 P x))
+               ((θ (fst (φ⁻¹-F s F 𝓧 P x))) , (m (φ⁻¹-F s F 𝓧 P x))))
+
+proj ε 𝓧 P x
+  = fst x
+proj (s ▸ mk-constr F G) (𝓧 , θ) (P , m)
+  = (proj s 𝓧 P)
+  , (λ x → snd (m (φ⁻¹-F s F 𝓧 P x)))
+
+-- Correctness of φ.
+module _
+  (s : Spec)
+  (F : Alg s ⇒ TypeCat)
+  (𝓧 : / Alg s /)
+  (P : Fam s 𝓧)
+  where
+
+  φ-φ⁻¹-F :
+    (x : F ⋆ (total s 𝓧 P))
+    → φ-F s F 𝓧 P (φ⁻¹-F s F 𝓧 P x) == x
+  φ-φ⁻¹-F x = idp
+
+  φ⁻¹-φ-F :
+    (x : Σ (F ⋆ 𝓧) (□-F s F 𝓧 P))
+    → φ⁻¹-F s F 𝓧 P (φ-F s F 𝓧 P x) == x
+  φ⁻¹-φ-F (.(Func.hom F (proj s 𝓧 P) x) , x , idp) = idp
+
+  module _
+    (G : ∫ (Alg s) F ⇒ TypeCat)
+    (x : F ⋆ 𝓧)
+    (y : □-F s F 𝓧 P x)
+    where
+    φ-φ⁻¹-G :
+      (p : G ⋆ (total s 𝓧 P , φ-F s F 𝓧 P (x , y)))
+      → φ-G s F G 𝓧 P x y (φ⁻¹-G s F G 𝓧 P x y p) == p
+    φ-φ⁻¹-G p = idp  
+
+    φ⁻¹-φ-G :
+      (p : Σ (G ⋆ (𝓧 , x)) (□-G s F G 𝓧 P x y))
+      → φ⁻¹-G s F G 𝓧 P x y (φ-G s F G 𝓧 P x y p) == p
+    φ⁻¹-φ-G (.(Func.hom G (proj s 𝓧 P , snd y) p) , p , idp) = idp

dep/FamCorrect.agda

@@ -0,0 +1,74 @@
+{-# OPTIONS --without-K #-}
+
+module dep.FamCorrect where
+
+open import lib.Basics
+open import Cat
+open import dep.Core
+open import dep.Fam
+open import dep.Fib
+open import Admit
+
+private
+  singleton-elim-2 :
+    (X : Set)
+    (P : X → Set)
+    (x : X)
+    → Σ (Σ X P) (λ y → fst y == x) ≃ P x
+  singleton-elim-2 X P x =
+    equiv
+      help-to
+      help-from
+      help-to-from
+      help-from-to
+      where
+        help-to : Σ (Σ X P) (λ y → fst y == x) → P x
+        help-to ((.x , p) , idp) = p
+        help-from : P x → Σ (Σ X P) (λ y → fst y == x)
+        help-from p = (x , p) , idp
+        help-to-from : (b : P x) → help-to (help-from b) == b
+        help-to-from b =  idp
+        help-from-to : (a : Σ (Σ X P) (λ y → fst y == x)) → help-from (help-to a) == a
+        help-from-to ((.x , p) , idp) = idp
+
+-- The preimage operation needs to be defined mutually with its
+-- correctness proof.
+preimage : (s : Spec) (𝓧 : / Alg s /) (𝓟 : Fib s 𝓧) → Fam s 𝓧
+
+fam-to-from : (s : Spec) (𝓧 : / Alg s /)
+  → (b : Fam s 𝓧) → preimage s 𝓧 (total s 𝓧 b , proj s 𝓧 b) == b
+
+fam-from-to-0 : (s : Spec) (𝓧 : / Alg s /)
+  → (𝓨 : / Alg s /) (𝓹 : Alg s [ 𝓨 , 𝓧 ])
+  → total s 𝓧 (preimage s 𝓧 (𝓨 , 𝓹)) == 𝓨
+
+fam-from-to-1 : (s : Spec) (𝓧 : / Alg s /)
+  → (𝓨 : / Alg s /) (𝓹 : Alg s [ 𝓨 , 𝓧 ])
+  → proj s 𝓧 (preimage s 𝓧 (𝓨 , 𝓹)) == 𝓹 [ (λ h → Alg s [ h , 𝓧 ]) ↓ fam-from-to-0 s 𝓧 𝓨 𝓹 ]
+
+fam-from-to : (s : Spec) (𝓧 : / Alg s /)
+  → (a : Fib s 𝓧) → total s 𝓧 (preimage s 𝓧 a) , proj s 𝓧 (preimage s 𝓧 a) == a
+
+preimage ε X (Y , p)
+  = hfiber p
+preimage (s ▸ mk-constr F G) (𝓧 , θ) ((𝓨 , ρ) , p , p₀)
+  = (preimage s 𝓧 (𝓨 , p)) , (λ { (x , z , h) → admit _ })
+
+fam-to-from ε X P = λ= (λ x → ua (singleton-elim-2 X P x))
+fam-to-from (s ▸ mk-constr F G) (𝓧 , θ) (𝓟 , m) = admit _
+
+fam-from-to-0 ε X Y p = admit _
+fam-from-to-0 (s ▸ mk-constr F G) 𝓧 a 𝓹 = admit _
+
+fam-from-to-1 ε X Y p = admit _
+fam-from-to-1 (s ▸ mk-constr F G) 𝓧 a 𝓹 = admit _
+
+fam-from-to s 𝓧 (𝓨 , 𝓹) = pair= (fam-from-to-0 s 𝓧 𝓨 𝓹) (fam-from-to-1 s 𝓧 𝓨 𝓹)
+
+fam-correct : (s : Spec) (𝓧 : / Alg s /) → Fib s 𝓧 == Fam s 𝓧
+fam-correct s 𝓧
+  = ua (equiv
+       (preimage s 𝓧)
+       (λ 𝓟 → total s 𝓧 𝓟 , proj s 𝓧 𝓟)
+       (fam-to-from s 𝓧)
+       (fam-from-to s 𝓧))

dep/Fib.agda

@@ -6,106 +6,7 @@ open import lib.Basics
 open import Cat
 open import dep.Core
 
--- Fibration over a given algebra
 Fib : (s : Spec) → / Alg s / → Type1
+Fib s 𝓧 = Σ (/ Alg s /) (λ 𝓨 → Alg s [ 𝓨 , 𝓧 ]) 
 
-□-F :
-  (s : Spec)
-  (F : Alg s ⇒ TypeCat)
-  (𝓧 : / Alg s /)
-  (P : Fib s 𝓧)
-  → F ⋆ 𝓧 → Type0
-
-□-G :
-  (s : Spec)
-  (F : Alg s ⇒ TypeCat)
-  (G : ∫ (Alg s) F ⇒ TypeCat)
-  (𝓧 : / Alg s /)
-  (P : Fib s 𝓧)
-  (x : F ⋆ 𝓧)
-  (y : □-F s F 𝓧 P x)
-  → G ⋆ (𝓧 , x) → Type0
-
-total :
-  (s : Spec)
-  (𝓧 : / Alg s /)
-  → Fib s 𝓧 → / Alg s /
-
-proj :
-  (s : Spec)
-  (𝓧 : / Alg s /)
-  (P : Fib s 𝓧)
-  → Alg s [ total s 𝓧 P , 𝓧 ]
-
-φ-F :
-  (s : Spec)
-  (F : Alg s ⇒ TypeCat)
-  (𝓧 : / Alg s /)
-  (P : Fib s 𝓧)
-  → Σ (F ⋆ 𝓧) (□-F s F 𝓧 P) → F ⋆ (total s 𝓧 P)
-
-φ⁻¹-F :
-  (s : Spec)
-  (F : Alg s ⇒ TypeCat)
-  (𝓧 : / Alg s /)
-  (P : Fib s 𝓧)
-  → F ⋆ (total s 𝓧 P) → Σ (F ⋆ 𝓧) (□-F s F 𝓧 P)
-
-φ-G :
-  (s : Spec)
-  (F : Alg s ⇒ TypeCat)
-  (G : ∫ (Alg s) F ⇒ TypeCat)
-  (𝓧 : / Alg s /)
-  (P : Fib s 𝓧)
-  (x : F ⋆ 𝓧)
-  (y : □-F s F 𝓧 P x)
-  → Σ (G ⋆ (𝓧 , x)) (□-G s F G 𝓧 P x y) → G ⋆ (total s 𝓧 P , φ-F s F 𝓧 P (x , y))
-
-φ⁻¹-G :
-  (s : Spec)
-  (F : Alg s ⇒ TypeCat)
-  (G : ∫ (Alg s) F ⇒ TypeCat)
-  (𝓧 : / Alg s /)
-  (P : Fib s 𝓧)
-  (x : F ⋆ 𝓧)
-  (y : □-F s F 𝓧 P x)
-  → G ⋆ (total s 𝓧 P , φ-F s F 𝓧 P (x , y)) → Σ (G ⋆ (𝓧 , x)) (□-G s F G 𝓧 P x y)
-
-Fib ε X
-  = X → Type0
-Fib (s ▸ mk-constr F G) (𝓧 , θ)
-  = Σ (Fib s 𝓧) (λ P → (x : Σ (F ⋆ 𝓧) (□-F s F 𝓧 P)) → □-G s F G 𝓧 P (fst x) (snd x) (θ (fst x)))
-
-□-F s F 𝓧 P x
-  = Σ (F ⋆ total s 𝓧 P) (λ y → (F ⋆⋆ proj s 𝓧 P) y == x)
-
-φ-F s F 𝓧 P (x , y , p)
-  = y
-
-φ⁻¹-F s F 𝓧 P x
-  = ((F ⋆⋆ proj s 𝓧 P) x) , (x , idp)
-
-□-G s F G 𝓧 P x y p
-  = Σ (G ⋆ (total s 𝓧 P) , φ-F s F 𝓧 P (x , y)) (λ q →
-      (G ⋆⋆ (proj s 𝓧 P) , snd y) q == p)
-
-φ-G s F G 𝓧 P x y (p , q , r)
-  = q
-
-φ⁻¹-G s F G 𝓧 P x y p
-  = ((G ⋆⋆ (proj s 𝓧 P) , (snd y)) p) , (p , idp)
-
-total ε X P
-  = Σ X P
-total (s ▸ mk-constr F G) (𝓧 , θ) (P , m)
-  = (total s 𝓧 P)
-  , (λ x → φ-G s F G 𝓧 P
-               (fst (φ⁻¹-F s F 𝓧 P x))
-               (snd (φ⁻¹-F s F 𝓧 P x))
-               ((θ (fst (φ⁻¹-F s F 𝓧 P x))) , (m (φ⁻¹-F s F 𝓧 P x))))
-
-proj ε 𝓧 P x
-  = fst x
-proj (s ▸ mk-constr F G) (𝓧 , θ) (P , m)
-  = (proj s 𝓧 P)
-  , (λ x → snd (m (φ⁻¹-F s F 𝓧 P x)))
+-- TODO: Equality stuff